1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jul 27 13:11:43 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jul 27 13:59:58 2022 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4    val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
     1.5    val get_cas: theory -> CAS_Def.T list
     1.6    val add_cas: CAS_Def.T list -> theory -> theory
     1.7 -  val get_ptyps: theory -> Probl_Def.store
     1.8 -  val add_pbts: (Probl_Def.T * References_Def.id) list -> theory -> theory
     1.9 +  val get_pbls: theory -> Probl_Def.store
    1.10 +  val add_pbls: (Probl_Def.T * References_Def.id) list -> theory -> theory
    1.11    val get_mets: theory -> Meth_Def.store
    1.12    val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.13    val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.14 @@ -120,8 +120,8 @@
    1.15      val extend = I;
    1.16      val merge = Store.merge;
    1.17      );
    1.18 -  fun get_ptyps thy = Data.get thy;
    1.19 -  fun add_pbts pbts thy = let
    1.20 +  fun get_pbls thy = Data.get thy;
    1.21 +  fun add_pbls pbts thy = let
    1.22            fun add_pbt (pbt as {guh,...}, pblID) =
    1.23                  (* the pblID has the leaf-element as first; better readability achieved *)
    1.24                  (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.25 @@ -252,7 +252,7 @@
    1.26  
    1.27  fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
    1.28  
    1.29 -fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
    1.30 +fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
    1.31  fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
    1.32  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.33  \<close>