# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1284394335 -7200
# Node ID d679c1f837a70b8bfabe6e7bc9dcccf9d330cbb8
# Parent  16d56796f5a01154a6b8c2235d898e014f9723d1
ref --> Unsynchronized.ref tuned.

there are differences in compiling via (1) Build_Isac.thy and via (2) ROOT.ML:
# (1) still accepts ref, while (2) requires Unsynchronized.ref
# (2) is more rigid in type checking (eg. "can't find a fixed record type")

diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:12:15 2010 +0200
@@ -57,18 +57,11 @@
 ML {* writeln "**** build math-engine complete **************************" *}
 
 ML {* writeln "**** build the Knowledge *********************************" *}
-(**)
-use_thy "Knowledge/Delete"
+(*use_thy "Knowledge/Delete"
   use_thy "Knowledge/Descript"
   use_thy "Knowledge/Atools"
   use_thy "Knowledge/Simplify"
   use_thy "Knowledge/Poly"
-
-ML {*
-val m = (1,[2]);
-#1 m;
-fst m;
-*}
   use_thy "Knowledge/Rational"
   use_thy "Knowledge/PolyMinus"
   use_thy "Knowledge/Equation"
@@ -89,16 +82,9 @@
   use_thy "Knowledge/EqSystem"
   use_thy "Knowledge/Biegelinie"
   use_thy "Knowledge/AlgEin"
- use_thy "Knowledge/Test"
-
-ML {* 111;
-*}
-
+  use_thy "Knowledge/Test"
+*)
 use_thy "Knowledge/Isac"
 
-
-text {*------------------------------------------*}
-(*
-*)
 end
 
diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/Frontend/states.sml
--- a/src/Tools/isac/Frontend/states.sml	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/Frontend/states.sml	Mon Sep 13 18:12:15 2010 +0200
@@ -149,8 +149,8 @@
 val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
 *)
 
-val states = 
-    ref ([]:(calcID * 
+val states = Unsynchronized.ref
+        ([]:(calcID * 
 	     (calcstate * 
 	      (iterID *       (*1 sets the 'active formula'*)
 	       pos'           (*for iterator of a user     *)
@@ -484,4 +484,4 @@
 |   [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])),
 |      (1, (((EmptyPtree, ([], Und)), []), [])),
 |      (3, (((EmptyPtree, ([], Und)), []), []))]
-*)
\ No newline at end of file
+*)
diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/Interpret/inform.sml
--- a/src/Tools/isac/Interpret/inform.sml	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/Interpret/inform.sml	Mon Sep 13 18:12:15 2010 +0200
@@ -42,7 +42,7 @@
        (Term.term * Term.term list) list ->
        pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
        (bool * Term.term) list  *)
-    val castab : castab ref
+    val castab : castab Unsynchronized.ref
     val compare_step :
        calcstate' -> Term.term -> string * calcstate'
    (* val concat_deriv :
diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Mon Sep 13 18:12:15 2010 +0200
@@ -3,7 +3,7 @@
    (c) due to copyright terms
 *) 
 
-theory Test imports Atools Rational Root Poly begin
+theory Test imports Atools Poly Rational Root Diff begin
  
 consts
 
diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/ProgLang/Script.thy
--- a/src/Tools/isac/ProgLang/Script.thy	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/ProgLang/Script.thy	Mon Sep 13 18:12:15 2010 +0200
@@ -185,7 +185,7 @@
 
 val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
 
-val tacpbl = ref
+val tacpbl = Unsynchronized.ref
   (distinct (remove op = "" (!tacs (*@ !subpbls*))));
 (*--^^^----- SHIFT? or delete ?*)
 
diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Mon Sep 13 17:21:22 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Mon Sep 13 18:12:15 2010 +0200
@@ -346,8 +346,9 @@
 (*rewrite orders, also stored in 'type met' and type 'and rls'
   The association list is required for 'rewrite.."rew_ord"..'
   WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
-val rew_ord' = 
-    ref ([]:(rew_ord' *        (*the key for the association list         *)
+val rew_ord' =
+    Unsynchronized.ref
+        ([]:(rew_ord' *        (*the key for the association list         *)
 	     (subst 	       (*the bound variables - they get high order*)
 	      -> (term * term) (*(t1, t2) to be compared                  *)
 	      -> bool))        (*if t1 <= t2 then true else false         *)