1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Apr 20 16:47:01 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 21 10:13:30 2020 +0200
     1.3 @@ -38,7 +38,6 @@
     1.4  ML_file "cas-def.sml"
     1.5  ML_file "thy-html.sml"
     1.6  
     1.7 -ML_file tracing.sml
     1.8  ML \<open>
     1.9  \<close> ML \<open>
    1.10  \<close> ML \<open>
    1.11 @@ -66,8 +65,8 @@
    1.12    val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
    1.13    val get_cas: theory -> CAS_Def.cas_elem list
    1.14    val add_cas: CAS_Def.cas_elem list -> theory -> theory
    1.15 -  val get_ptyps: theory -> Probl_Def.ptyps
    1.16 -  val add_pbts: (Probl_Def.pbt * Spec.pblID) list -> theory -> theory
    1.17 +  val get_ptyps: theory -> Probl_Def.store
    1.18 +  val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
    1.19    val get_mets: theory -> Meth_Def.mets
    1.20    val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
    1.21    val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
    1.22 @@ -109,8 +108,8 @@
    1.23    fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
    1.24  
    1.25    structure Data = Theory_Data (
    1.26 -    type T = Probl_Def.ptyps;
    1.27 -    val empty = [Probl_Def.e_Ptyp];
    1.28 +    type T = Probl_Def.store;
    1.29 +    val empty = [Probl_Def.empty_store];
    1.30      val extend = I;
    1.31      val merge = Store.merge_ptyps;
    1.32      );
    1.33 @@ -118,7 +117,7 @@
    1.34    fun add_pbts pbts thy = let
    1.35            fun add_pbt (pbt as {guh,...}, pblID) =
    1.36                  (* the pblID has the leaf-element as first; better readability achieved *)
    1.37 -                (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_pblguh_unique guh (Data.get thy) else ();
    1.38 +                (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.39                    rev pblID |> Store.insrt pblID pbt);
    1.40          in Data.map (fold add_pbt pbts) thy end;
    1.41  
    1.42 @@ -242,9 +241,9 @@
    1.43        1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
    1.44  fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
    1.45        (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
    1.46 -val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.pbts2str;
    1.47 +val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
    1.48  fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
    1.49 -fun pbt_ord ({guh = guh'1, ...} : Probl_Def.pbt, {guh = guh'2, ...} : Probl_Def.pbt) = string_ord (guh'1, guh'2);
    1.50 +fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
    1.51  fun sort_kestore_ptyp' _ [] = []
    1.52    | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
    1.53       ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))