1.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Wed Jan 22 20:23:31 2014 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Wed Jan 22 23:31:59 2014 +0100
     1.3 @@ -468,7 +468,7 @@
     1.4  (*.the pblID has the leaf-element as first; better readability achieved;.*)
     1.5  fun store_pbt (pbt as {guh,...}, pblID) = 
     1.6      (if (!check_guhs_unique) then check_pblguh_unique guh (get_ptyps ()) else ();
     1.7 -     ptyps:= insrt pblID pbt (rev pblID) (get_ptyps ()));
     1.8 +     ptyps:= insrt pblID pbt (rev pblID) (! ptyps));
     1.9  
    1.10  (*.the metID has the root-element as first; compare 'fun store_pbt'.*)
    1.11  fun store_met (met as {guh,...}, metID) =

     2.1 --- a/src/Tools/isac/KEStore.thy	Wed Jan 22 20:23:31 2014 +0100
     2.2 +++ b/src/Tools/isac/KEStore.thy	Wed Jan 22 23:31:59 2014 +0100
     2.3 @@ -111,7 +111,7 @@
     2.4  
     2.5  fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
     2.6  
     2.7 -fun get_ptyps () = !ptyps;
     2.8 +fun get_ptyps () = ! ptyps (*KEStore_Elems.get_ptyps @{theory}*);
     2.9  *}
    2.10  setup {* KEStore_Elems.add_rlss 
    2.11    [("e_rls", (Context.theory_name @{theory}, e_rls)), 

     3.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Jan 22 20:23:31 2014 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Jan 22 23:31:59 2014 +0100
     3.3 @@ -30,8 +30,6 @@
     3.4    ],
     3.5    e_rls, SOME "solve (e_e::bool, v_v::int)",
     3.6    [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
     3.7 -show_ptyps();
     3.8 -get_pbt ["diophantine","equation"];
     3.9  *}
    3.10  setup {* KEStore_Elems.store_pbts
    3.11    [(prep_pbt thy "pbl_equ_dio" [] e_pblID