1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Aug 17 21:48:38 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Tue Aug 17 21:57:40 2021 +0200
     1.3 @@ -459,12 +459,8 @@
     1.4  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     1.5  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     1.6  val t = TermC.str2term "sqrt 4";
     1.7 +Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
     1.8  
     1.9 -(* error-from-Skip_Proof.make_thm: inherited errors are marked TOODOO.1 in test/*
    1.10 - exception TYPE raised (line 169 of "consts.ML"): Illegal type
    1.11 -   for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
    1.12 -      Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
    1.13 -( **)
    1.14  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
    1.15    ((ThyC.get_theory "Isac_Knowledge"),
    1.16      ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);