1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -68,6 +68,8 @@
     1.4  *)
     1.5  signature KESTORE_ELEMS =
     1.6  sig
     1.7 +  val get_rew_ord: theory -> Rewrite_Ord.rew_ord list
     1.8 +  val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
     1.9    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    1.10    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    1.11    val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
    1.12 @@ -87,11 +89,20 @@
    1.13    val set_ref_thy: theory -> unit
    1.14  end;                               
    1.15  
    1.16 -structure KEStore_Elems: KESTORE_ELEMS =
    1.17 +structure KEStore_Elems(**): KESTORE_ELEMS(**) =
    1.18  struct
    1.19    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
    1.20  
    1.21    structure Data = Theory_Data (
    1.22 +    type T = (string * (LibraryC.subst -> term * term -> bool)) list;
    1.23 +    val empty = [];
    1.24 +    val extend = I;
    1.25 +    val merge = merge Rewrite_Ord.equal;
    1.26 +    );  
    1.27 +  fun get_rew_ord thy = Data.get thy
    1.28 +  fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
    1.29 +
    1.30 +  structure Data = Theory_Data (
    1.31      type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
    1.32      val empty = [];
    1.33      val extend = I;
    1.34 @@ -183,7 +194,7 @@
    1.35    val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
    1.36    fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
    1.37    fun get_ref_thy () = Synchronized.value cur_thy;
    1.38 -end;
    1.39 +(**)end(**);
    1.40  \<close>
    1.41  
    1.42  
    1.43 @@ -242,6 +253,12 @@
    1.44  ML \<open>
    1.45  val get_ref_thy = KEStore_Elems.get_ref_thy;
    1.46  
    1.47 +fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
    1.48 +  | assoc' ((keyi, xi) :: pairs, key) =
    1.49 +    if key = keyi then SOME xi else assoc' (pairs, key);
    1.50 +fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
    1.51 +  handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
    1.52 +
    1.53  fun assoc_rls (rls' : Rule_Set.id) =
    1.54    case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
    1.55      SOME (_, rls) => rls