1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Apr 28 19:39:06 2020 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Apr 29 09:03:01 2020 +0200
     1.3 @@ -45,10 +45,10 @@
     1.4  (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
     1.5  val t = str2term "((1+2)*4/3)^^^2";
     1.6  val thy = @{theory};
     1.7 -val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn;
     1.8 -val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn;
     1.9 -val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn;
    1.10 -val pow =    ("Prog_Expr.pow"  ,eval_binop "#power_") : string * Exec_Def.eval_fn;
    1.11 +val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
    1.12 +val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
    1.13 +val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    1.14 +val pow =    ("Prog_Expr.pow"  ,eval_binop "#power_") : string * Eval_Def.eval_fn;
    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 @{theory} isa_fn t;