1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Sep 07 15:01:17 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Sep 07 15:06:50 2022 +0200
     1.3 @@ -259,12 +259,6 @@
     1.4  fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
     1.5    handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
     1.6  
     1.7 -fun assoc_rls (rls' : Rule_Set.id) =
     1.8 -  case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
     1.9 -    SOME (_, rls) => rls
    1.10 -  | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
    1.11 -    "TODO exception hierarchy needs to be established.")
    1.12 -
    1.13  fun get_rls ctxt (rls' : Rule_Set.id) =
    1.14    case AList.lookup (op =) (KEStore_Elems.get_rlss (Proof_Context.theory_of ctxt )) rls' of
    1.15      SOME (_, rls) => rls
    1.16 @@ -272,12 +266,6 @@
    1.17      (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
    1.18      "\nTODO exception hierarchy needs to be established.")
    1.19  
    1.20 -fun assoc_rls' thy (rls' : Rule_Set.id) =
    1.21 -  case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
    1.22 -    SOME (_, rls) => rls
    1.23 -  | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
    1.24 -    "TODO exception hierarchy needs to be established.")
    1.25 -
    1.26  fun assoc_calc thy calID = let
    1.27      fun ass ([], key) =
    1.28            raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))