1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sun Aug 08 15:21:33 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Aug 09 11:19:25 2021 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4  
     1.5   val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
     1.6  case rewrite_set_ thy false rls t of
     1.7 -  SOME (t', _) =>   (*WAS "x + 2" WITH OLD numerals TOODOO?*)
     1.8 +  SOME (t', _) =>
     1.9      if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.10  | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
    1.11  
    1.12 @@ -204,7 +204,6 @@
    1.13   Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
    1.14   val t = (Thm.term_of o the o (TermC.parse thy))  "x + (- 1 + -3) / 2";
    1.15  val SOME (res, []) = rewrite_set_ thy false rls t;
    1.16 -                 (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
    1.17  if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (- 1 + -3) / 2  changed";
    1.18  "x + (-4) / 2";						
    1.19  (*
    1.20 @@ -468,12 +467,16 @@
    1.21  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
    1.22    ((ThyC.get_theory "Isac_Knowledge"),
    1.23      ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
    1.24 +
    1.25  val SOME (thmid, t) =
    1.26    (*case*) get_pair thy op_ eval_fn ct (*of*);
    1.27 +(*+*)val "sqrt 4 = 2" = UnparseC.term t;
    1.28 +
    1.29  (** )
    1.30 +      Skip_Proof.make_thm thy t;
    1.31 +
    1.32    exception TYPE raised (line 169 of "consts.ML"): Illegal type
    1.33     for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
    1.34 -      Skip_Proof.make_thm thy t
    1.35  ( **)
    1.36  
    1.37  "----------- fun power -------------------------------------------------------------------------";