1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 11:28:20 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 12:26:08 2020 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
     1.5    val get_mets: theory -> Meth_Def.store
     1.6    val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
     1.7 -  val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
     1.8 +  val get_thes: theory -> (Thy_Html.thydata Store.node) list
     1.9    val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.10    val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    1.11    val get_ref_thy: unit -> theory
    1.12 @@ -111,34 +111,34 @@
    1.13      type T = Probl_Def.store;
    1.14      val empty = [Probl_Def.empty_store];
    1.15      val extend = I;
    1.16 -    val merge = Store.merge_ptyps;
    1.17 +    val merge = Store.merge;
    1.18      );
    1.19    fun get_ptyps thy = Data.get thy;
    1.20    fun add_pbts pbts thy = let
    1.21            fun add_pbt (pbt as {guh,...}, pblID) =
    1.22                  (* the pblID has the leaf-element as first; better readability achieved *)
    1.23                  (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.24 -                  rev pblID |> Store.insrt pblID pbt);
    1.25 +                  rev pblID |> Store.insert pblID pbt);
    1.26          in Data.map (fold add_pbt pbts) thy end;
    1.27  
    1.28    structure Data = Theory_Data (
    1.29      type T = Meth_Def.store;
    1.30      val empty = [Meth_Def.empty_store];
    1.31      val extend = I;
    1.32 -    val merge = Store.merge_ptyps;
    1.33 +    val merge = Store.merge;
    1.34      );
    1.35    val get_mets = Data.get;
    1.36    fun add_mets mets thy = let
    1.37            fun add_met (met as {guh,...}, metID) =
    1.38                  (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.39 -                  Store.insrt metID met metID);
    1.40 +                  Store.insert metID met metID);
    1.41          in Data.map (fold add_met mets) thy end;
    1.42  
    1.43    structure Data = Theory_Data (
    1.44 -    type T = (Thy_Html.thydata Store.ptyp) list;
    1.45 +    type T = (Thy_Html.thydata Store.node) list;
    1.46      val empty = [];
    1.47      val extend = I;
    1.48 -    val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
    1.49 +    val merge = Store.merge; (* relevant for store_thm, store_rls *)
    1.50      );                                                              
    1.51    fun get_thes thy = Data.get thy
    1.52    fun add_thes thes thy = let
    1.53 @@ -148,11 +148,11 @@
    1.54      let
    1.55        fun update_elem (theID, fillpats) =
    1.56          let
    1.57 -          val hthm = Store.get_py (Data.get thy) theID theID
    1.58 +          val hthm = Store.get (Data.get thy) theID theID
    1.59            val hthm' = Thy_Html.update_hthm hthm fillpats
    1.60              handle ERROR _ =>
    1.61                error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
    1.62 -        in Store.update_ptyps theID theID hthm' end
    1.63 +        in Store.update theID theID hthm' end
    1.64      in Data.map (fold update_elem fis) thy end
    1.65  
    1.66    val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
    1.67 @@ -237,21 +237,21 @@
    1.68    (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
    1.69  
    1.70  fun count_kestore_ptyps [] = 0
    1.71 -  | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
    1.72 +  | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
    1.73        1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
    1.74 -fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
    1.75 +fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
    1.76        (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
    1.77  val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
    1.78 -fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
    1.79 +fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
    1.80  fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
    1.81  fun sort_kestore_ptyp' _ [] = []
    1.82 -  | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
    1.83 -     ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
    1.84 +  | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
    1.85 +     ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
    1.86         :: sort_kestore_ptyp' ordfun ps');
    1.87  val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
    1.88  
    1.89  fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
    1.90 -fun check_kestore_met (mp: Meth_Def.T Store.ptyp) =
    1.91 +fun check_kestore_met (mp: Meth_Def.T Store.node) =
    1.92        check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
    1.93  fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
    1.94  val sort_kestore_met = sort_kestore_ptyp' met_ord;