1.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Fri Jan 24 18:03:27 2014 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Sat Jan 25 21:06:58 2014 +0100
     1.3 @@ -376,7 +376,7 @@
     1.4  fun app_ptyp x = app_py (get_ptyps ()) x;
     1.5  
     1.6  (*TODO: search generalized for subthy*)
     1.7 -fun get_pbt (pblID:pblID) = get_py (!ptyps) pblID (rev pblID)
     1.8 +fun get_pbt (pblID:pblID) = get_py (get_ptyps ()) pblID (rev pblID)
     1.9  (* get_pbt thy ["1"];
    1.10     get_pbt thy ["21","2"];
    1.11     *)
    1.12 @@ -424,7 +424,7 @@
    1.13  	in case nodes [] guh (get_ptyps ()) of
    1.14  	       SOME id => rev id
    1.15  	     | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
    1.16 -				    "not found in (!ptyps)")
    1.17 +				    "not found in ptyps")
    1.18  	end
    1.19        | "met_" =>
    1.20  	let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jan 24 18:03:27 2014 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Sat Jan 25 21:06:58 2014 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  text {* This theory collects data of theorems and axioms defined and used in ISAC *}
     2.5  
     2.6  ML {*
     2.7 -  writeln ("======= length (KEStore_Elems = " ^
     2.8 +  (*writeln ("======= length (KEStore_Elems = " ^
     2.9      (KEStore_Elems.get_ptyps @{theory} |> count_kestore_ptyps |> string_of_int));
    2.10    writeln ("======= length (! ptyps) = " ^
    2.11      (count_kestore_ptyps (! ptyps) |> string_of_int));
    2.12 @@ -31,7 +31,7 @@
    2.13    writeln "\n\n======= ! ptyps ordered =======";
    2.14    ! ptyps |> rev (*!!!!!*) |> sort_kestore_ptyp |> sort ptyp_ord
    2.15      |> map check_kestore_ptyp |> enumerate_strings |> sort string_ord |> map writeln;
    2.16 -  writeln "======= end ! ptyps =======";
    2.17 +  writeln "======= end ! ptyps =======";*)
    2.18  *}
    2.19  
    2.20  ML {*

     3.1 --- a/test/Tools/isac/Interpret/ptyps.sml	Fri Jan 24 18:03:27 2014 +0100
     3.2 +++ b/test/Tools/isac/Interpret/ptyps.sml	Sat Jan 25 21:06:58 2014 +0100
     3.3 @@ -143,7 +143,7 @@
     3.4  i.e. there is no common fun for pbls and mets ?!?*)
     3.5  
     3.6  coll_pblguhs (!ptyps);
     3.7 -sort string_ord (coll_pblguhs (!ptyps));
     3.8 +sort string_ord (coll_pblguhs (get_ptyps ()));
     3.9  show_pblguhs ();
    3.10  sort_pblguhs ();
    3.11  
    3.12 @@ -153,7 +153,7 @@
    3.13  "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
    3.14  (* ERROR: Exception Bind raised *)
    3.15  val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
    3.16 -     Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);
    3.17 +     Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
    3.18  
    3.19  (*
    3.20  nodes [] guh1 (!ptyps);
    3.21 @@ -166,7 +166,7 @@
    3.22       ::
    3.23       Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
    3.24       ::
    3.25 -     _ ) = (!ptyps);
    3.26 +     _ ) = (get_ptyps ());
    3.27  (*
    3.28  nodes [] guh3 (!ptyps);
    3.29  nodes [] guh21 (!ptyps);

     4.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Fri Jan 24 18:03:27 2014 +0100
     4.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Sat Jan 25 21:06:58 2014 +0100
     4.3 @@ -117,9 +117,9 @@
     4.4  "----- ERROR Illegal reference to internal variable: 'Pure_' -----";
     4.5  val path = "/tmp/"; 
     4.6  "~~~~~ fun pbls2file, args:"; val (p:path) = (path ^ "pbl/");
     4.7 -!ptyps; (*not = []*)
     4.8 +get_ptyps (); (*not = []*)
     4.9  "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
    4.10 -  (p, []: string list, [0], pbl2file, (!ptyps));
    4.11 +  (p, []: string list, [0], pbl2file, (get_ptyps ()));
    4.12  "~~~~~ fun node, args:"; val (pa:path, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
    4.13  val po' = lev_on po;
    4.14  wfn (*= pbl2file*)