1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 12:22:37 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 15:37:39 2020 +0200
     1.3 @@ -34,8 +34,6 @@
     1.4  ML_file "celem-7.sml"  (*cas_elem*)
     1.5  ML_file "celem-8.sml"  (*thydata*)
     1.6  ML_file "celem-91.sml" (*check_guhs_unique*)
     1.7 -ML_file "celem-92.sml" (**)
     1.8 -ML_file "celem-93.sml" (**)
     1.9  
    1.10  ML_file calcelems.sml
    1.11  ML_file tracing.sml
    1.12 @@ -112,34 +110,34 @@
    1.13      type T = Celem.ptyps;
    1.14      val empty = [Celem.e_Ptyp];
    1.15      val extend = I;
    1.16 -    val merge = Celem.merge_ptyps;
    1.17 +    val merge = Celem1.merge_ptyps;
    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 (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
    1.24 -                  rev pblID |> Celem.insrt pblID pbt);
    1.25 +                  rev pblID |> Celem1.insrt 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 = Celem.mets;
    1.30      val empty = [Celem.e_Mets];
    1.31      val extend = I;
    1.32 -    val merge = Celem.merge_ptyps;
    1.33 +    val merge = Celem1.merge_ptyps;
    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 (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
    1.39 -                  Celem.insrt metID met metID);
    1.40 +                  Celem1.insrt 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 = (Celem.thydata Celem1.ptyp) list;
    1.45      val empty = [];
    1.46      val extend = I;
    1.47 -    val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
    1.48 +    val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
    1.49      );                                                              
    1.50    fun get_thes thy = Data.get thy
    1.51    fun add_thes thes thy = let
    1.52 @@ -149,11 +147,11 @@
    1.53      let
    1.54        fun update_elem (theID, fillpats) =
    1.55          let
    1.56 -          val hthm = Celem.get_py (Data.get thy) theID theID
    1.57 +          val hthm = Celem1.get_py (Data.get thy) theID theID
    1.58            val hthm' = Celem.update_hthm hthm fillpats
    1.59              handle ERROR _ =>
    1.60                error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
    1.61 -        in Celem.update_ptyps theID theID hthm' end
    1.62 +        in Celem1.update_ptyps theID theID hthm' end
    1.63      in Data.map (fold update_elem fis) thy end
    1.64  
    1.65    val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
    1.66 @@ -241,7 +239,7 @@
    1.67    | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
    1.68        1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
    1.69  fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
    1.70 -      (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
    1.71 +      (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
    1.72  val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
    1.73  fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
    1.74  fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
    1.75 @@ -260,7 +258,7 @@
    1.76  fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
    1.77  fun write_thes thydata_list =
    1.78    thydata_list 
    1.79 -    |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
    1.80 +    |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
    1.81      |> map pair2str
    1.82      |> map writeln
    1.83  \<close>