1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 14:36:27 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 16:01:53 2020 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4    fun add_pbts pbts thy = let
     1.5            fun add_pbt (pbt as {guh,...}, pblID) =
     1.6                  (* the pblID has the leaf-element as first; better readability achieved *)
     1.7 -                (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
     1.8 +                (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
     1.9                    rev pblID |> Store.insert pblID pbt);
    1.10          in Data.map (fold add_pbt pbts) thy end;
    1.11  
    1.12 @@ -130,7 +130,7 @@
    1.13    val get_mets = Data.get;
    1.14    fun add_mets mets thy = let
    1.15            fun add_met (met as {guh,...}, metID) =
    1.16 -                (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.17 +                (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.18                    Store.insert metID met metID);
    1.19          in Data.map (fold add_met mets) thy end;
    1.20