1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 10:53:04 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 11:28:20 2020 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
     1.5    val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
     1.6    val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
     1.7 -  val get_cas: theory -> CAS_Def.cas_elem list
     1.8 -  val add_cas: CAS_Def.cas_elem list -> theory -> theory
     1.9 +  val get_cas: theory -> CAS_Def.T list
    1.10 +  val add_cas: CAS_Def.T list -> theory -> theory
    1.11    val get_ptyps: theory -> Probl_Def.store
    1.12    val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
    1.13    val get_mets: theory -> Meth_Def.store
    1.14 @@ -102,10 +102,10 @@
    1.15      type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
    1.16      val empty = [];
    1.17      val extend = I;
    1.18 -    val merge = merge CAS_Def.cas_eq;
    1.19 +    val merge = merge CAS_Def.equal;
    1.20      );                                                              
    1.21    fun get_cas thy = Data.get thy
    1.22 -  fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
    1.23 +  fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
    1.24  
    1.25    structure Data = Theory_Data (
    1.26      type T = Probl_Def.store;
    1.27 @@ -232,7 +232,7 @@
    1.28  fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
    1.29  
    1.30  (* we avoid term_to_string''' defined later *)
    1.31 -fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
    1.32 +fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
    1.33    "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
    1.34    (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
    1.35