1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Aug 23 12:33:10 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Aug 23 14:24:06 2021 +0200
     1.3 @@ -484,18 +484,11 @@
     1.4  (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
     1.5  *)
     1.6  
     1.7 +val NONE = adhoc_thm @{theory} eval_ t;
     1.8 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
     1.9  val NONE =
    1.10 -           adhoc_thm @{theory} eval_ t;
    1.11 -"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
    1.12 -val SOME ("#divide_e~1_2", t') =
    1.13    (*case*) get_pair thy op_ eval_fn t (*of*);
    1.14  
    1.15 -(*+*)UnparseC.term t = "- 1 / 2";
    1.16 -(*+*)UnparseC.term t' = "- 1 / 2 = - 1 / 2"; "HOL.Trueprop";
    1.17 -
    1.18 -if t = (TermC.rhs o HOLogic.dest_Trueprop) t' 
    1.19 -then () else error "fun adhoc_thm + fun eval_cancel CHANGED";
    1.20 -
    1.21  
    1.22  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.23  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";