diff -r 454fad8ab67a -r 3a746a4bb75f src/Tools/isac/BaseDefinitions/Know_Store.thy
--- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 10:53:04 2020 +0200
+++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 11:28:20 2020 +0200
@@ -63,8 +63,8 @@
   val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
   val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
   val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
-  val get_cas: theory -> CAS_Def.cas_elem list
-  val add_cas: CAS_Def.cas_elem list -> theory -> theory
+  val get_cas: theory -> CAS_Def.T list
+  val add_cas: CAS_Def.T list -> theory -> theory
   val get_ptyps: theory -> Probl_Def.store
   val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
   val get_mets: theory -> Meth_Def.store
@@ -102,10 +102,10 @@
     type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
     val empty = [];
     val extend = I;
-    val merge = merge CAS_Def.cas_eq;
+    val merge = merge CAS_Def.equal;
     );                                                              
   fun get_cas thy = Data.get thy
-  fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
+  fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
 
   structure Data = Theory_Data (
     type T = Probl_Def.store;
@@ -232,7 +232,7 @@
 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
 
 (* we avoid term_to_string''' defined later *)
-fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
+fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
   "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
   (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";