1.1 --- a/doc-isac/mat-eng-en.tex	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/doc-isac/mat-eng-en.tex	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -216,9 +216,9 @@
     1.4     *** . . Free ( #3, )
     1.5     val it = () : unit
     1.6     ML>
     1.7 -   ML> atomty;
     1.8 +   ML> TermC.atom_trace_detail \@\{context\};
     1.9     val it = fn : theory -> term -> unit
    1.10 -   ML> atomty thy t;
    1.11 +   ML> TermC.atom_trace_detail \@\{context\} t;
    1.12     *** -------------
    1.13     *** Const ( op +, [real, real] => real)
    1.14     *** . Free ( a, real)
    1.15 @@ -255,7 +255,7 @@
    1.16  Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots
    1.17  {\footnotesize\begin{verbatim}
    1.18     ML> (*-4-*) val thy = RatArith.thy;
    1.19 -   ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.20 +   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.21     *** -------------
    1.22     *** Free ( d_d, [real, real] => real)
    1.23     *** . Free ( x, real)
    1.24 @@ -265,7 +265,7 @@
    1.25     val it = () : unit
    1.26     ML>
    1.27     ML> (*-6-*) val thy = Differentiate.thy;
    1.28 -   ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.29 +   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.30     *** -------------
    1.31     *** Const ( Differentiate.d_d, [real, real] => real)
    1.32     *** . Free ( x, real)
    1.33 @@ -866,10 +866,10 @@
    1.34     *** . Free ( c, )
    1.35     val it = () : unit
    1.36     ML>
    1.37 -   ML> free2var;
    1.38 +   ML> mk_Var;
    1.39     val it = fn : term -> term
    1.40     ML>
    1.41 -   ML> val pat = free2var p;
    1.42 +   ML> val pat = mk_Var p;
    1.43     val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
    1.44     ML> Sign.string_of_term (sign_of thy) pat;
    1.45     val it = "?a * ?b ^^^ #2 = ?c" : cterm' 
    1.46 @@ -884,7 +884,7 @@
    1.47     *** . Var ((c, 0), )
    1.48     val it = () : unit
    1.49  \end{verbatim}}%size % $ 
    1.50 -Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:
    1.51 +Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt mk_Var}. This format of the pattern is necessary in order to obtain results like these:
    1.52  {\footnotesize\begin{verbatim}
    1.53     ML> matches thy t pat;
    1.54     val it = true : bool