1.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Thu Jun 10 12:53:02 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Thu Jun 10 17:06:32 2021 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4    type calc
     1.5    eqtype calID
     1.6    eqtype errpatID
     1.7 -  type rew_ord
     1.8 -  type rew_ord'
     1.9 -  type rew_ord_
    1.10 -  type eval_fn
    1.11 +  type rew_ord' = string
    1.12 +  type rew_ord_ = (term * term) list -> term * term -> bool
    1.13 +  type rew_ord = rew_ord' * rew_ord_
    1.14 +  type eval_fn = string -> term -> theory -> (string * term) option
    1.15  
    1.16    datatype rule_set =
    1.17         Empty
    1.18 @@ -41,7 +41,7 @@
    1.19  struct
    1.20  (**)
    1.21  
    1.22 -type eval_fn = (string -> term -> theory -> (string * term) option);
    1.23 +type eval_fn = string -> term -> theory -> (string * term) option;
    1.24  
    1.25  type rew_ord' = string;
    1.26  type rew_ord_ = (term * term) list -> term * term -> bool;
    1.27 @@ -61,14 +61,14 @@
    1.28    | Thm of            (* theorem associated with the identifier for reflection        *)
    1.29        string *        (* needless since Thm.get_name_hint                             *)
    1.30          Thm.thm       (* see TODO CLEANUP Thm                                         *)
    1.31 -  | Eval of       (* evaluation by rewriting                                      *)
    1.32 +  | Eval of           (* evaluation by rewriting                                      *)
    1.33        string *        (* unique identifier for the evaluation function                *)
    1.34    	    eval_fn       (* evaluation function in ML code                               *)
    1.35    | Cal1 of string *  (* applied once to whole term or lhs/rhs of an eqality          *)
    1.36    	  eval_fn         (* evaluation function in ML code                               *)
    1.37    | Rls_ of rule_set  (* rule sets may be nested                                      *)
    1.38  and program =         (* program for Lucas-Interpretation                             *)
    1.39 -    Empty_Prog          (* DEPRECATED: needless after removal of Rfuns                  *)
    1.40 +    Empty_Prog        (* DEPRECATED: needless after removal of Rfuns                  *)
    1.41    | Prog of term      (* Lucas-Interpretation works on Isabelle's terms               *)
    1.42    | Rfuns of          (* DEPRECATED, replaced by Auto_Prog                            *)
    1.43      {init_state :     (* initialise for reverse rewriting by the Interpreter          *)
    1.44 @@ -115,7 +115,7 @@
    1.45       rules: rule list,
    1.46       errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy              *)
    1.47       scr: program}    (* DEPRECATED: intersteps are created on the fly now            *)
    1.48 -  | Sequence of        (* a sequence of rules to be tried only once                    *)
    1.49 +  | Sequence of       (* a sequence of rules to be tried only once                    *)
    1.50      {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
    1.51       calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
    1.52    | Rrls of           (* ML-functions within rewriting, _ONE_ redex rewritten per call*)