1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 28 19:39:06 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 29 09:03:01 2020 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  ML_file unparseC.sml
     1.5  ML_file "rule-def.sml"
     1.6  ML_file "thmC-def.sml"
     1.7 -ML_file "exec-def.sml"       (*rename identifiers by use of struct.id*)
     1.8 +ML_file "eval-def.sml"       (*rename identifiers by use of struct.id*)
     1.9  ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)
    1.10  ML_file rule.sml
    1.11  ML_file "error-pattern-def.sml"
    1.12 @@ -61,8 +61,8 @@
    1.13  sig
    1.14    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    1.15    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    1.16 -  val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
    1.17 -  val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
    1.18 +  val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
    1.19 +  val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
    1.20    val get_cas: theory -> CAS_Def.T list
    1.21    val add_cas: CAS_Def.T list -> theory -> theory
    1.22    val get_ptyps: theory -> Probl_Def.store
    1.23 @@ -90,13 +90,13 @@
    1.24    fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
    1.25  
    1.26    structure Data = Theory_Data (
    1.27 -    type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
    1.28 +    type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
    1.29      val empty = [];
    1.30      val extend = I;
    1.31 -    val merge = merge Exec_Def.calc_eq;
    1.32 +    val merge = merge Eval_Def.calc_eq;
    1.33      );                                                              
    1.34    fun get_calcs thy = Data.get thy
    1.35 -  fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
    1.36 +  fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
    1.37  
    1.38    structure Data = Theory_Data (
    1.39      type T = (term * (Spec.T * (term list -> (term * term list) list))) list;