1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Jul 31 12:39:07 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Jul 31 13:23:38 2022 +0200
     1.3 @@ -73,9 +73,9 @@
     1.4    val get_cas: theory -> CAS_Def.T list
     1.5    val add_cas: CAS_Def.T list -> theory -> theory
     1.6    val get_pbls: theory -> Probl_Def.store
     1.7 -  val add_pbls: (Probl_Def.T * References_Def.id) list -> theory -> theory
     1.8 +  val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
     1.9    val get_mets: theory -> Meth_Def.store
    1.10 -  val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.11 +  val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.12    val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.13    val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.14    val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.15 @@ -121,12 +121,13 @@
    1.16      val merge = Store.merge;
    1.17      );
    1.18    fun get_pbls thy = Data.get thy;
    1.19 -  fun add_pbls pbts thy = let
    1.20 -          fun add_pbt (pbt as {guh,...}, pblID) =
    1.21 -                (* the pblID has the leaf-element as first; better readability achieved *)
    1.22 -                (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.23 -                  rev pblID |> Store.insert pblID pbt);
    1.24 -        in Data.map (fold add_pbt pbts) thy end;
    1.25 +  fun add_pbls ctxt pbts thy =
    1.26 +    let
    1.27 +      fun add_pbt (pbt as {guh,...}, pblID) =
    1.28 +        (* the pblID has the leaf-element as first; better readability achieved *)
    1.29 +        (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.30 +          rev pblID |> Store.insert pblID pbt);
    1.31 +    in Data.map (fold add_pbt pbts) thy end;
    1.32  
    1.33    structure Data = Theory_Data (
    1.34      type T = Meth_Def.store;
    1.35 @@ -135,11 +136,12 @@
    1.36      val merge = Store.merge;
    1.37      );
    1.38    val get_mets = Data.get;
    1.39 -  fun add_mets mets thy = let
    1.40 -          fun add_met (met as {guh,...}, metID) =
    1.41 -                (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.42 -                  Store.insert metID met metID);
    1.43 -        in Data.map (fold add_met mets) thy end;
    1.44 +  fun add_mets ctxt mets thy =
    1.45 +    let
    1.46 +      fun add_met (met as {guh,...}, metID) =
    1.47 +        (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.48 +          Store.insert metID met metID);
    1.49 +    in Data.map (fold add_met mets) thy end;
    1.50  
    1.51    structure Data = Theory_Data (
    1.52      type T = (Thy_Write.thydata Store.node) list;