1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4  "----------- check calculate bottom up ------------------";
     1.5  "----------- check calculate bottom up ------------------";
     1.6  (*-------------- eval_cancel works: *)
     1.7 - Rewrite.trace_on := false;
     1.8 + Rewrite.trace_on := false; (*true false*)
     1.9   val thy = @{theory Test};
    1.10   val rls = Test_simplify;
    1.11   val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
    1.12 @@ -170,7 +170,7 @@
    1.13      if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.14  | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
    1.15  
    1.16 - Rewrite.trace_on:=false; (*=true3.6.03*)
    1.17 + Rewrite.trace_on := false; (*true false*)
    1.18  
    1.19  (*--- Rewrite.trace_on before correction of ... --------------------
    1.20   val ct = "(-3 + 2 * x + - 1) / 2";
    1.21 @@ -460,7 +460,7 @@
    1.22  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.23  val t = TermC.str2term "sqrt 4";
    1.24  
    1.25 -(* TODO.ThmC.numerals_to_Free 1 * )
    1.26 +(* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * )
    1.27    exception TYPE raised (line 169 of "consts.ML"): Illegal type
    1.28     for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
    1.29        Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t