1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -31,8 +31,8 @@
     1.4  *)
     1.5  signature KESTORE_ELEMS =
     1.6  sig
     1.7 -  val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list
     1.8 -  val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
     1.9 +  val get_rlss: theory -> (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list
    1.10 +  val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
    1.11    val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
    1.12    val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
    1.13    val get_cas: theory -> Celem.cas_elem list
    1.14 @@ -53,13 +53,13 @@
    1.15    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
    1.16  
    1.17    structure Data = Theory_Data (
    1.18 -    type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list;
    1.19 +    type T = (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list;
    1.20      val empty = [];
    1.21      val extend = I;
    1.22 -    val merge = Rule_Set.merge_rlss;
    1.23 +    val merge = Rule_Set.to_kestore;
    1.24      );  
    1.25    fun get_rlss thy = Data.get thy
    1.26 -  fun add_rlss rlss = Data.map (union_overwrite Rule_Set.rls_eq rlss)
    1.27 +  fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
    1.28  
    1.29    structure Data = Theory_Data (
    1.30      type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
    1.31 @@ -141,13 +141,13 @@
    1.32  ML \<open>
    1.33  val get_ref_thy = KEStore_Elems.get_ref_thy;
    1.34  
    1.35 -fun assoc_rls (rls' : Rule_Set.rls') =
    1.36 +fun assoc_rls (rls' : Rule_Set.identifier) =
    1.37    case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
    1.38      SOME (_, rls) => rls
    1.39    | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
    1.40      "TODO exception hierarchy needs to be established.")
    1.41  
    1.42 -fun assoc_rls' thy (rls' : Rule_Set.rls') =
    1.43 +fun assoc_rls' thy (rls' : Rule_Set.identifier) =
    1.44    case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
    1.45      SOME (_, rls) => rls
    1.46    | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
    1.47 @@ -174,7 +174,7 @@
    1.48  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.49  \<close>
    1.50  setup \<open>KEStore_Elems.add_rlss 
    1.51 -  [("e_rls", (Context.theory_name @{theory}, Rule_Set.e_rls)), 
    1.52 +  [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), 
    1.53    ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
    1.54  
    1.55  section \<open>determine sequence of main parts in thehier\<close>
    1.56 @@ -201,7 +201,7 @@
    1.57  fun check_kestore_rls (rls', (thyID, rls)) =
    1.58    "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
    1.59  
    1.60 -fun check_kestore_calc ((id, (c, _)) : Rule_Set.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
    1.61 +fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
    1.62  
    1.63  (* we avoid term_to_string''' defined later *)
    1.64  fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =