1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 17:21:14 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 18:29:33 2022 +0200
     1.3 @@ -49,10 +49,10 @@
     1.4  val t = TermC.str2term "((1+2)*4/3) \<up> 2";
     1.5  val thy = @{theory};
     1.6  val ctxt = Proof_Context.init_global @{theory}
     1.7 -val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.eval_fn;
     1.8 -val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn;
     1.9 -val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    1.10 -val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
    1.11 +val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.ml_fun;
    1.12 +val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.ml_fun;
    1.13 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.ml_fun;
    1.14 +val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.ml_fun;
    1.15  
    1.16  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
    1.17  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
    1.18 @@ -435,7 +435,7 @@
    1.19  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.20  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.21  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.22 -val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
    1.23 +val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : Eval.ml_fun): Eval.ml;
    1.24  val t = @{term "- 1 / 2 ::real"};
    1.25  (* 
    1.26    ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals