1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 16:43:53 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Apr 20 15:54:19 2020 +0200
     1.3 @@ -29,15 +29,14 @@
     1.4  ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
     1.5  ML_file "rule-set.sml"
     1.6  
     1.7 -ML_file "celem-0.sml"  (*survey Celem.*)
     1.8  ML_file "store.sml"
     1.9 +ML_file "check-unique.sml"
    1.10  ML_file "specification.sml"
    1.11  ML_file "celem-4.sml"  (*pat*)
    1.12  ML_file "celem-5.sml"  (*ptyps*)
    1.13  ML_file "celem-6.sml"  (*mets*)
    1.14  ML_file "celem-7.sml"  (*cas_elem*)
    1.15  ML_file "celem-8.sml"  (*thydata*)
    1.16 -ML_file "celem-91.sml" (*check_guhs_unique*)
    1.17  
    1.18  ML_file tracing.sml
    1.19  ML \<open>
    1.20 @@ -119,7 +118,7 @@
    1.21    fun add_pbts 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 (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
    1.25 +                (if (!Check_Unique.check_guhs_unique) then Celem5.check_pblguh_unique guh (Data.get thy) else ();
    1.26                    rev pblID |> Store.insrt pblID pbt);
    1.27          in Data.map (fold add_pbt pbts) thy end;
    1.28  
    1.29 @@ -132,7 +131,7 @@
    1.30    val get_mets = Data.get;
    1.31    fun add_mets mets thy = let
    1.32            fun add_met (met as {guh,...}, metID) =
    1.33 -                (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
    1.34 +                (if (!Check_Unique.check_guhs_unique) then Celem6.check_metguh_unique guh (Data.get thy) else ();
    1.35                    Store.insrt metID met metID);
    1.36          in Data.map (fold add_met mets) thy end;
    1.37