1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 17:21:14 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 18:29:33 2022 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4    val add_rew_ord: Rewrite_Ord.T list -> theory -> theory
     1.5    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
     1.6    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
     1.7 -  val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
     1.8 -  val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
     1.9 +  val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
    1.10 +  val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
    1.11    val get_cas: theory -> CAS_Def.T list
    1.12    val add_cas: CAS_Def.T list -> theory -> theory
    1.13    val get_pbls: theory -> Probl_Def.store
    1.14 @@ -110,13 +110,13 @@
    1.15    fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
    1.16  
    1.17    structure Data = Theory_Data (
    1.18 -    type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
    1.19 +    type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
    1.20      val empty = [];
    1.21      val extend = I;
    1.22 -    val merge = merge Eval_Def.calc_eq;
    1.23 +    val merge = merge Eval_Def.equal;
    1.24      );                                                              
    1.25    fun get_calcs thy = Data.get thy
    1.26 -  fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.calc_eq) calcs)
    1.27 +  fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) calcs)
    1.28  
    1.29    structure Data = Theory_Data (
    1.30      type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
    1.31 @@ -234,9 +234,9 @@
    1.32            val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
    1.33            val set_data =
    1.34              ML_Context.expression (Input.pos_of source)
    1.35 -              (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
    1.36 +              (ml "Theory.setup (Eval_Def.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")
    1.37              |> Context.theory_map;
    1.38 -          val eval = Eval_Def.the_data (set_data thy);
    1.39 +          val eval = Eval_Def.ml_fun_from_store (set_data thy);
    1.40          in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
    1.41  
    1.42  in end;

     2.1 --- a/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 17:21:14 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 18:29:33 2022 +0200
     2.3 @@ -7,24 +7,24 @@
     2.4  *)
     2.5  signature EVALUATE__DEFINITION =
     2.6  sig
     2.7 -(*eqtype const_id*)
     2.8 -  eqtype calID
     2.9 -(*type ml*)
    2.10 -  type cal
    2.11 -(*eqtype.prog_id*)
    2.12 -  eqtype prog_calcID
    2.13 -(*type ml_from_prog*)
    2.14 -  type calc_elem
    2.15 -(*val equal*)
    2.16 -  val calc_eq: calc_elem * calc_elem -> bool
    2.17 -(*type ml_fun*)
    2.18 -  type eval_fn = Rule_Def.eval_fn
    2.19 -(*val ml_fun_empty*)
    2.20 -  val e_evalfn: Rule_Def.eval_fn
    2.21 -(*val to_store*)
    2.22 -  val set_data: eval_fn -> theory -> theory
    2.23 -(*val from_store*)
    2.24 -  val the_data: theory -> eval_fn
    2.25 +  eqtype const_id
    2.26 +(*eqtype calID*)
    2.27 +  type ml
    2.28 +(*type cal*)
    2.29 +  eqtype prog_id
    2.30 +(*eqtype prog_calcID*)
    2.31 +  type ml_from_prog
    2.32 +(*type calc_elem*)
    2.33 +  val equal: ml_from_prog * ml_from_prog -> bool
    2.34 +(*val calc_eq: ml_from_prog * ml_from_prog -> bool*)
    2.35 +  type ml_fun = Rule_Def.eval_fn
    2.36 +(*type eval_fn = Rule_Def.eval_fn*)
    2.37 +  val ml_fun_empty: ml_fun
    2.38 +(*val e_evalfn: ml_fun*)
    2.39 +  val ml_fun_to_store: ml_fun -> theory -> theory
    2.40 +(*val set_data: ml_fun -> theory -> theory*)
    2.41 +  val ml_fun_from_store: theory -> ml_fun
    2.42 +(*val the_data: theory -> ml_fun*)
    2.43  (**)
    2.44  end
    2.45  
    2.46 @@ -33,27 +33,29 @@
    2.47  struct
    2.48  (**)
    2.49  
    2.50 -type calID = Rule_Def.eval_const_id
    2.51 -type prog_calcID = string;
    2.52 -(* op in isa-term "Const(op,_)" *)
    2.53 -type cal = Rule_Def.eval_const_id * Rule_Def.eval_fn;
    2.54 -type calc_elem =  (* fun calculate_ fetches the evaluation-function via this list *)
    2.55 -  prog_calcID *   (* a simple identifier used in programs                    *)
    2.56 -  (Rule_Def.eval_const_id *        (* a long identifier used in Const                         *)
    2.57 -    Rule_Def.eval_fn)      (* an ML function                                          *)
    2.58 -fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    2.59 +type const_id = Rule_Def.eval_const_id (* op in Isabelle term "Const( op, _)" *)
    2.60 +type ml_fun = Rule_Def.eval_fn
    2.61 +type ml = const_id * ml_fun;
    2.62 +
    2.63 +type prog_id = string; (* accepted by partial_function in method*)
    2.64 +type ml_from_prog =  (* fun calculate_ fetches the evaluation-function via this list *)
    2.65 +  prog_id *   (* a simple identifier used in programs                    *)
    2.66 +  (const_id *        (* a long identifier used in Const                         *)
    2.67 +    ml_fun)      (* an ML function                                          *)
    2.68 +
    2.69 +fun equal ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    2.70    if pi1 = pi2
    2.71 -  then if ci1 = ci2 then true else raise ERROR ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
    2.72 +  then if ci1 = ci2 then true else raise ERROR ("equal: " ^ ci1 ^ " <> " ^ ci2)
    2.73    else false
    2.74  
    2.75  (* eval function calling sml code during rewriting.
    2.76 -Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
    2.77 +Unifying "type ml" and "type calc" would make Lucas-Interpretation more efficient,
    2.78    see "fun rule2stac": instead of 
    2.79 -    Eval: calID * eval_fn -> rule
    2.80 +    Eval: const_id * eval_fn -> rule
    2.81    would be better
    2.82 -    Eval: prog_calcID * (calID * eval_fn)) -> rule*)
    2.83 +    Eval: prog_id * (const_id * eval_fn)) -> rule*)
    2.84  type eval_fn = Rule_Def.eval_fn
    2.85 -fun e_evalfn (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option;
    2.86 +fun ml_fun_empty (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option;
    2.87  
    2.88  
    2.89  (* theory data for Isar command 'calculation' *)
    2.90 @@ -66,7 +68,7 @@
    2.91    fun merge _ = NONE;
    2.92  );
    2.93  
    2.94 -val set_data = Data.put o SOME;
    2.95 -val the_data = the o Data.get;
    2.96 +val ml_fun_to_store = Data.put o SOME;
    2.97 +val ml_fun_from_store = the o Data.get;
    2.98  
    2.99  end

     3.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 17:21:14 2022 +0200
     3.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 18:29:33 2022 +0200
     3.3 @@ -11,6 +11,7 @@
     3.4  (*eqtype calID*)
     3.5    type eval_ml_from_prog
     3.6  (*type calc*)
     3.7 +  type eval_fn = string -> term -> Proof.context -> (string * term) option
     3.8  
     3.9    eqtype errpatID
    3.10  
    3.11 @@ -18,7 +19,6 @@
    3.12    type rew_ord_function = LibraryC.subst -> term * term -> bool
    3.13    type rew_ord_T = rew_ord_id * rew_ord_function
    3.14  
    3.15 -  type eval_fn = string -> term -> Proof.context -> (string * term) option
    3.16  
    3.17    datatype rule_set =
    3.18         Empty

     4.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 24 17:21:14 2022 +0200
     4.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 24 18:29:33 2022 +0200
     4.3 @@ -123,7 +123,7 @@
     4.4  	    preconds = union (op =) pc1 pc2,	    
     4.5  	    erls = merge (merge_ids er1 er2) er1 er2,
     4.6  	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
     4.7 -	    calc = union Eval_Def.calc_eq ca1 ca2,
     4.8 +	    calc = union Eval_Def.equal ca1 ca2,
     4.9  		  rules = union Rule.equal rs1 rs2,
    4.10        errpatts = union (op =) eps1 eps2}
    4.11    | merge id
    4.12 @@ -136,7 +136,7 @@
    4.13  	    preconds = union (op =) pc1 pc2,	    
    4.14  	    erls = merge (merge_ids er1 er2) er1 er2,
    4.15  	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
    4.16 -	    calc = union Eval_Def.calc_eq ca1 ca2,
    4.17 +	    calc = union Eval_Def.equal ca1 ca2,
    4.18  		  rules = union Rule.equal rs1 rs2,
    4.19        errpatts = union (op =) eps1 eps2}
    4.20    | merge id _ _ = raise ERROR ("merge: \"" ^ id ^ 

     5.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 17:21:14 2022 +0200
     5.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 18:29:33 2022 +0200
     5.3 @@ -18,10 +18,20 @@
     5.4  
     5.5    val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
     5.6      string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
     5.7 +(** )
     5.8 +  val get_eval: string -> Pos.pos -> Ctree.ctree ->
     5.9 +    string * ThyC.id * (Eval.ml_fun)
    5.10 +( *original*)
    5.11    val get_eval: string -> Pos.pos ->Ctree.ctree ->
    5.12      string * ThyC.id * (string * Rule_Def.eval_fn)
    5.13 +(**)
    5.14 +
    5.15  \<^isac_test>\<open>
    5.16 +(**)
    5.17    val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.eval_ml_from_prog list
    5.18 +(*original* )
    5.19 +  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.eval_ml_from_prog list
    5.20 +( **)
    5.21  \<close>
    5.22  end
    5.23  
    5.24 @@ -71,7 +81,7 @@
    5.25  	    in
    5.26  	      case opt of
    5.27  	        SOME isa_fn => ("OK", thy', isa_fn)
    5.28 -	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
    5.29 +	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.ml_fun_empty))
    5.30  	    end
    5.31      else 
    5.32  		  let
    5.33 @@ -80,7 +90,7 @@
    5.34  		  in
    5.35  		    case assoc (scr_isa_fns, scrop) of
    5.36  		      SOME isa_fn => ("OK",thy',isa_fn)
    5.37 -		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
    5.38 +		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.ml_fun_empty))
    5.39  		  end
    5.40    end;
    5.41  

     6.1 --- a/src/Tools/isac/Interpret/thy-read.sml	Wed Aug 24 17:21:14 2022 +0200
     6.2 +++ b/src/Tools/isac/Interpret/thy-read.sml	Wed Aug 24 18:29:33 2022 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  sig
     6.5    val thy_containing_thm : string -> string * string
     6.6    val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
     6.7 -  val thy_containing_cal : ThyC.id -> Eval_Def.prog_calcID -> string * string
     6.8 +  val thy_containing_cal : ThyC.id -> Eval_Def.prog_id -> string * string
     6.9  
    6.10    val from_store : Thy_Write.theID -> Thy_Write.thydata                                  (* for inform.sml *)
    6.11  \<^isac_test>\<open>

     7.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 24 17:21:14 2022 +0200
     7.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 24 18:29:33 2022 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  signature REWRITE =
     7.5  sig
     7.6    exception NO_REWRITE
     7.7 -  val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
     7.8 +  val calculate_: Proof.context -> string * Eval_Def.ml_fun -> term -> (term * (string * thm)) option
     7.9    val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
    7.10    val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
    7.11    val eval_true_: Proof.context -> Rule_Set.T -> term -> bool

     8.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 24 17:21:14 2022 +0200
     8.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 24 18:29:33 2022 +0200
     8.3 @@ -33,7 +33,7 @@
     8.4      val subpbl: string -> string list -> term
     8.5      val stacpbls: term -> term list
     8.6      val op_of_calc: term -> string
     8.7 -    val get_calcs: theory -> term -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
     8.8 +    val get_calcs: theory -> term -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
     8.9      val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
    8.10      val gen: theory -> term -> Rule_Set.T -> term
    8.11  \<^isac_test>\<open>

     9.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 17:21:14 2022 +0200
     9.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 18:29:33 2022 +0200
     9.3 @@ -7,8 +7,9 @@
     9.4  
     9.5  signature EVALUATE =
     9.6  sig
     9.7 -(*type ml*)
     9.8 -(*type ml_from_prog*)
     9.9 +  type ml
    9.10 +  type ml_fun
    9.11 +  type ml_from_prog
    9.12  
    9.13    val is_num: term -> bool
    9.14    val calc_equ: string -> int * int -> bool
    9.15 @@ -18,13 +19,13 @@
    9.16    val gcd: int -> int -> int
    9.17    val sqrt: int -> int
    9.18    val cancel_int: int * int -> int * (int * int)
    9.19 -  val adhoc_thm: Proof.context -> Eval_Def.cal -> term -> (string * thm) option
    9.20 -  val adhoc_thm1_: Proof.context -> Eval_Def.cal -> term -> (string * thm) option
    9.21 +  val adhoc_thm: Proof.context -> Eval_Def.ml -> term -> (string * thm) option
    9.22 +  val adhoc_thm1_: Proof.context -> Eval_Def.ml -> term -> (string * thm) option
    9.23    val norm: term -> term
    9.24    val popt2str: ('a * term) option -> string
    9.25    val int_of_numeral: term -> int
    9.26  \<^isac_test>\<open>
    9.27 -  val get_pair: Proof.context -> string -> Eval_Def.eval_fn -> term -> (string * term) option
    9.28 +  val get_pair: Proof.context -> string -> Eval_Def.ml_fun -> term -> (string * term) option
    9.29    val mk_rule: term list * term * term -> term
    9.30    val divisors: int -> int list
    9.31    val doubles: int list -> int list
    9.32 @@ -36,8 +37,9 @@
    9.33  struct
    9.34  (**)
    9.35  
    9.36 -(*type ml = Eval_Def.ml*)
    9.37 -(*type ml_from_prog = Eval_Def.ml_from_prog*)
    9.38 +type ml = Eval_Def.ml
    9.39 +type ml_fun = Eval_Def.ml_fun
    9.40 +type ml_from_prog = Eval_Def.ml_from_prog
    9.41  
    9.42  val is_num = can HOLogic.dest_number;
    9.43  
    9.44 @@ -117,7 +119,7 @@
    9.45  fun trace_calc4 ctxt str t1 t2 =
    9.46    if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
    9.47  
    9.48 -fun get_pair (*1*)ctxt  op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) =   (* unary fns *)
    9.49 +fun get_pair (*1*)ctxt  op_ (ef: Eval_Def.ml_fun) (t as (Const (op0, _) $ arg)) =   (* unary fns *)
    9.50      if op_ = op0 then 
    9.51        let val popt = ef op_ t ctxt  
    9.52        in case popt of SOME _ => popt | NONE => get_pair ctxt  op_ ef arg end

    10.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Wed Aug 24 17:21:14 2022 +0200
    10.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Wed Aug 24 18:29:33 2022 +0200
    10.3 @@ -14,6 +14,6 @@
    10.4      else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
    10.5  \<close>
    10.6  
    10.7 -setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Eval_Def.e_evalfn))]\<close>
    10.8 +setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Eval_Def.ml_fun_empty))]\<close>
    10.9  
   10.10  end

    11.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Wed Aug 24 17:21:14 2022 +0200
    11.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Wed Aug 24 18:29:33 2022 +0200
    11.3 @@ -9,8 +9,8 @@
    11.4  sig
    11.5    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    11.6    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    11.7 -  val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
    11.8 -  val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
    11.9 +  val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
   11.10 +  val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
   11.11    (*etc*)
   11.12  end;                               
   11.13  
   11.14 @@ -28,7 +28,7 @@
   11.15  
   11.16    val calc_eq = rls_eq
   11.17    structure Data = Theory_Data (
   11.18 -    type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
   11.19 +    type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
   11.20      val empty = [];
   11.21      val extend = I;
   11.22      val merge = merge calc_eq;

    12.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 17:21:14 2022 +0200
    12.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 18:29:33 2022 +0200
    12.3 @@ -49,10 +49,10 @@
    12.4  val t = TermC.str2term "((1+2)*4/3) \<up> 2";
    12.5  val thy = @{theory};
    12.6  val ctxt = Proof_Context.init_global @{theory}
    12.7 -val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.eval_fn;
    12.8 -val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn;
    12.9 -val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
   12.10 -val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
   12.11 +val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.ml_fun;
   12.12 +val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.ml_fun;
   12.13 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.ml_fun;
   12.14 +val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.ml_fun;
   12.15  
   12.16  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
   12.17  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
   12.18 @@ -435,7 +435,7 @@
   12.19  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
   12.20  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
   12.21  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
   12.22 -val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
   12.23 +val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : Eval.ml_fun): Eval.ml;
   12.24  val t = @{term "- 1 / 2 ::real"};
   12.25  (* 
   12.26    ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals