1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Aug 09 11:19:25 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Aug 09 14:20:20 2021 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  "----------- calculate (2 * x is_const) -----------------";
     1.5  "----------- fun get_pair: examples ------------------------------------------------------------";
     1.6  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
     1.7 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     1.8  "----------- fun power -------------------------------------------------------------------------";
     1.9  "----------- fun divisors ----------------------------------------------------------------------";
    1.10  "----------- fun doubles, fun squfact ----------------------------------------------------------";
    1.11 @@ -459,8 +460,8 @@
    1.12  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.13  val t = TermC.str2term "sqrt 4";
    1.14  
    1.15 -(* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * )
    1.16 -  exception TYPE raised (line 169 of "consts.ML"): Illegal type
    1.17 +(* error-from-Skip_Proof.make_thm: inherited errors are marked TOODOO.1 in test/*
    1.18 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
    1.19     for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
    1.20        Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
    1.21  ( **)