1.1 --- a/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 19:02:19 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 19:12:17 2022 +0200
     1.3 @@ -8,24 +8,18 @@
     1.4  signature EVALUATE__DEFINITION =
     1.5  sig
     1.6    eqtype const_id
     1.7 -(*eqtype calID*)
     1.8 +  type ml_fun = Rule_Def.eval_fn
     1.9 +  val ml_fun_empty: ml_fun
    1.10    type ml
    1.11 -(*type cal*)
    1.12 +
    1.13    eqtype prog_id
    1.14 -(*eqtype prog_calcID*)
    1.15    type ml_from_prog
    1.16 -(*type calc_elem*)
    1.17 +
    1.18    val equal: ml_from_prog * ml_from_prog -> bool
    1.19 -(*val calc_eq: ml_from_prog * ml_from_prog -> bool*)
    1.20 -  type ml_fun = Rule_Def.eval_fn
    1.21 -(*type eval_fn = Rule_Def.eval_fn*)
    1.22 -  val ml_fun_empty: ml_fun
    1.23 -(*val e_evalfn: ml_fun*)
    1.24 +
    1.25    val ml_fun_to_store: ml_fun -> theory -> theory
    1.26 -(*val set_data: ml_fun -> theory -> theory*)
    1.27    val ml_fun_from_store: theory -> ml_fun
    1.28 -(*val the_data: theory -> ml_fun*)
    1.29 -(**)
    1.30 +
    1.31  end
    1.32  
    1.33  (**)
    1.34 @@ -35,13 +29,14 @@
    1.35  
    1.36  type const_id = Rule_Def.eval_const_id (* op in Isabelle term "Const( op, _)" *)
    1.37  type ml_fun = Rule_Def.eval_fn
    1.38 +fun ml_fun_empty (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option;
    1.39  type ml = const_id * ml_fun;
    1.40  
    1.41 -type prog_id = string; (* accepted by partial_function in method*)
    1.42 -type ml_from_prog =  (* fun calculate_ fetches the evaluation-function via this list *)
    1.43 -  prog_id *   (* a simple identifier used in programs                    *)
    1.44 -  (const_id *        (* a long identifier used in Const                         *)
    1.45 -    ml_fun)      (* an ML function                                          *)
    1.46 +type prog_id = string; (* accepted by partial_function in method *)
    1.47 +type ml_from_prog =  (* fetched by fun calculate_                   *)
    1.48 +  prog_id *          (* a simple identifier used in programs        *)
    1.49 +  (const_id *        (* a long identifier used in Const             *)
    1.50 +    ml_fun)          (* ML function for evaluation within rewriting *)
    1.51  
    1.52  fun equal ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    1.53    if pi1 = pi2
    1.54 @@ -54,15 +49,13 @@
    1.55      Eval: const_id * eval_fn -> rule
    1.56    would be better
    1.57      Eval: prog_id * (const_id * eval_fn)) -> rule*)
    1.58 -type eval_fn = Rule_Def.eval_fn
    1.59 -fun ml_fun_empty (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option;
    1.60  
    1.61  
    1.62  (* theory data for Isar command 'calculation' *)
    1.63  
    1.64  structure Data = Theory_Data
    1.65  (
    1.66 -  type T = eval_fn option;
    1.67 +  type T = ml_fun option;
    1.68    val empty = NONE;
    1.69    val extend = I;
    1.70    fun merge _ = NONE;

     2.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 19:02:19 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 19:12:17 2022 +0200
     2.3 @@ -8,9 +8,7 @@
     2.4  signature RULE_DEFINITION =
     2.5  sig
     2.6    eqtype eval_const_id
     2.7 -(*eqtype calID*)
     2.8    type eval_ml_from_prog
     2.9 -(*type calc*)
    2.10    type eval_fn = string -> term -> Proof.context -> (string * term) option
    2.11  
    2.12    eqtype errpatID