1.1 --- a/src/Tools/isac/KEStore.thy	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/src/Tools/isac/KEStore.thy	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -26,8 +26,7 @@
     1.4    val get_cas: theory -> cas_elem list
     1.5    val add_cas: cas_elem list -> theory -> theory
     1.6    val get_ptyps: theory -> ptyps
     1.7 -  val store_pbts: (pbt * pblID) list -> theory -> theory
     1.8 -  val add_pbt: (pbt * pblID) -> theory -> theory
     1.9 +  val add_pbts: (pbt * pblID) list -> theory -> theory
    1.10    (*etc*)
    1.11  end;                               
    1.12  
    1.13 @@ -69,13 +68,12 @@
    1.14      val merge = merge_ptyps;
    1.15      );
    1.16    fun get_ptyps thy = Data.get thy;
    1.17 -  fun store_pbts pbts = let
    1.18 -          fun store_pbts' (pbt, pblID) = rev pblID |> insrt pblID pbt;
    1.19 -        in fold store_pbts' pbts |> Data.map end;
    1.20 -  (* the pblID has the leaf-element as first; better readability achieved *)
    1.21 -  fun add_pbt (pbt as {guh,...}, pblID) = 
    1.22 -    (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();
    1.23 -    Data.map (insrt pblID pbt (rev pblID)))
    1.24 +  fun add_pbts pbts thy = let
    1.25 +          fun add_pbt (pbt as {guh,...}, pblID) =
    1.26 +                (* the pblID has the leaf-element as first; better readability achieved *)
    1.27 +                (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else ();
    1.28 +                  rev pblID |> insrt pblID pbt);
    1.29 +        in Data.map (fold add_pbt pbts) thy end;
    1.30  
    1.31    (*etc*)
    1.32  end;
    1.33 @@ -116,10 +114,9 @@
    1.34  
    1.35  fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
    1.36  
    1.37 -fun get_ptyps () = ! ptyps 
    1.38 +fun get_ptyps () = ! ptyps;
    1.39  (*SWITCH:
    1.40 -fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*);
    1.41 -val store_pbts = KEStore_Elems.store_pbts;
    1.42 +fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*)
    1.43  
    1.44  (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel 
    1.45    SETUP ..* KEStore_Elems.add_pbt (.....) *..