1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 10:13:30 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 10:53:04 2020 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4    val add_cas: CAS_Def.cas_elem list -> theory -> theory
     1.5    val get_ptyps: theory -> Probl_Def.store
     1.6    val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
     1.7 -  val get_mets: theory -> Meth_Def.mets
     1.8 -  val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
     1.9 +  val get_mets: theory -> Meth_Def.store
    1.10 +  val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
    1.11    val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
    1.12    val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.13    val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    1.14 @@ -122,15 +122,15 @@
    1.15          in Data.map (fold add_pbt pbts) thy end;
    1.16  
    1.17    structure Data = Theory_Data (
    1.18 -    type T = Meth_Def.mets;
    1.19 -    val empty = [Meth_Def.e_Mets];
    1.20 +    type T = Meth_Def.store;
    1.21 +    val empty = [Meth_Def.empty_store];
    1.22      val extend = I;
    1.23      val merge = Store.merge_ptyps;
    1.24      );
    1.25    val get_mets = Data.get;
    1.26    fun add_mets mets thy = let
    1.27            fun add_met (met as {guh,...}, metID) =
    1.28 -                (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else ();
    1.29 +                (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.30                    Store.insrt metID met metID);
    1.31          in Data.map (fold add_met mets) thy end;
    1.32  
    1.33 @@ -250,10 +250,10 @@
    1.34         :: sort_kestore_ptyp' ordfun ps');
    1.35  val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
    1.36  
    1.37 -fun metguh2str ({guh,...} : Meth_Def.met) = guh : string;
    1.38 -fun check_kestore_met (mp: Meth_Def.met Store.ptyp) =
    1.39 +fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
    1.40 +fun check_kestore_met (mp: Meth_Def.T Store.ptyp) =
    1.41        check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
    1.42 -fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2);
    1.43 +fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
    1.44  val sort_kestore_met = sort_kestore_ptyp' met_ord;
    1.45  
    1.46  fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes