1.1 --- a/doc-isac/mat-eng.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/doc-isac/mat-eng.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  TermC.parse_test @{context} "a + b * 3";
     1.5  val term = TermC.parse_test @{context} "a + b * 3";
     1.6  atomt term;
     1.7 -atomty term;
     1.8 +TermC.atom_trace_detail @{context} term;
     1.9  
    1.10  (*2.3. Theories and parsing*)
    1.11  
    1.12 @@ -92,7 +92,7 @@
    1.13       Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
    1.14       Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
    1.15  : Theory.theory
    1.16 -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.17 +> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.18  
    1.19  ***
    1.20  *** Free (d_d, [real, real] => real)
    1.21 @@ -118,7 +118,7 @@
    1.22       Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
    1.23       PolyEq, LogExp, Diff} : Theory.theory
    1.24  
    1.25 -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.26 +> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.27  
    1.28  ***
    1.29  *** Const (Diff.d_d, [real, real] => real)
    1.30 @@ -176,8 +176,8 @@
    1.31   ?Compiler.Control.Print.stringDepth;
    1.32   atomt;
    1.33   atomt t; 
    1.34 - atomty;
    1.35 - atomty thy t;
    1.36 + TermC.atom_trace_detail @{context};
    1.37 + TermC.atom_trace_detail @{context} t;
    1.38  (*Give it a try: the mathematics knowledge grows*)
    1.39   parse HOL.thy "2^^^3";
    1.40   parse HOL.thy "d_d x (a + x)";
    1.41 @@ -187,9 +187,9 @@
    1.42   ?parse Differentiate.thy "#2^^^#3";
    1.43  (*don't trust the string representation*)
    1.44   ?val thy = RatArith.thy;
    1.45 - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.46 + ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.47   ?val thy = Differentiate.thy;
    1.48 - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.49 + ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    1.50  
    1.51  (*2.4. Converting terms*)
    1.52   term_of;
    1.53 @@ -384,8 +384,8 @@
    1.54   val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
    1.55   val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
    1.56   atomt p;
    1.57 - free2var;
    1.58 - val pat = free2var p;
    1.59 + mk_Var;
    1.60 + val pat = mk_Var p;
    1.61   matches thy t pat;
    1.62  
    1.63   val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";