1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 17:21:22 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:12:15 2010 +0200
     1.3 @@ -57,18 +57,11 @@
     1.4  ML {* writeln "**** build math-engine complete **************************" *}
     1.5  
     1.6  ML {* writeln "**** build the Knowledge *********************************" *}
     1.7 -(**)
     1.8 -use_thy "Knowledge/Delete"
     1.9 +(*use_thy "Knowledge/Delete"
    1.10    use_thy "Knowledge/Descript"
    1.11    use_thy "Knowledge/Atools"
    1.12    use_thy "Knowledge/Simplify"
    1.13    use_thy "Knowledge/Poly"
    1.14 -
    1.15 -ML {*
    1.16 -val m = (1,[2]);
    1.17 -#1 m;
    1.18 -fst m;
    1.19 -*}
    1.20    use_thy "Knowledge/Rational"
    1.21    use_thy "Knowledge/PolyMinus"
    1.22    use_thy "Knowledge/Equation"
    1.23 @@ -89,16 +82,9 @@
    1.24    use_thy "Knowledge/EqSystem"
    1.25    use_thy "Knowledge/Biegelinie"
    1.26    use_thy "Knowledge/AlgEin"
    1.27 - use_thy "Knowledge/Test"
    1.28 -
    1.29 -ML {* 111;
    1.30 -*}
    1.31 -
    1.32 +  use_thy "Knowledge/Test"
    1.33 +*)
    1.34  use_thy "Knowledge/Isac"
    1.35  
    1.36 -
    1.37 -text {*------------------------------------------*}
    1.38 -(*
    1.39 -*)
    1.40  end
    1.41  

     2.1 --- a/src/Tools/isac/Frontend/states.sml	Mon Sep 13 17:21:22 2010 +0200
     2.2 +++ b/src/Tools/isac/Frontend/states.sml	Mon Sep 13 18:12:15 2010 +0200
     2.3 @@ -149,8 +149,8 @@
     2.4  val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
     2.5  *)
     2.6  
     2.7 -val states = 
     2.8 -    ref ([]:(calcID * 
     2.9 +val states = Unsynchronized.ref
    2.10 +        ([]:(calcID * 
    2.11  	     (calcstate * 
    2.12  	      (iterID *       (*1 sets the 'active formula'*)
    2.13  	       pos'           (*for iterator of a user     *)
    2.14 @@ -484,4 +484,4 @@
    2.15  |   [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])),
    2.16  |      (1, (((EmptyPtree, ([], Und)), []), [])),
    2.17  |      (3, (((EmptyPtree, ([], Und)), []), []))]
    2.18 -*)
    2.19 \ No newline at end of file
    2.20 +*)

     3.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Sep 13 17:21:22 2010 +0200
     3.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Sep 13 18:12:15 2010 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4         (Term.term * Term.term list) list ->
     3.5         pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
     3.6         (bool * Term.term) list  *)
     3.7 -    val castab : castab ref
     3.8 +    val castab : castab Unsynchronized.ref
     3.9      val compare_step :
    3.10         calcstate' -> Term.term -> string * calcstate'
    3.11     (* val concat_deriv :

     4.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Sep 13 17:21:22 2010 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Sep 13 18:12:15 2010 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4     (c) due to copyright terms
     4.5  *) 
     4.6  
     4.7 -theory Test imports Atools Rational Root Poly begin
     4.8 +theory Test imports Atools Poly Rational Root Diff begin
     4.9   
    4.10  consts
    4.11  

     5.1 --- a/src/Tools/isac/ProgLang/Script.thy	Mon Sep 13 17:21:22 2010 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/Script.thy	Mon Sep 13 18:12:15 2010 +0200
     5.3 @@ -185,7 +185,7 @@
     5.4  
     5.5  val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
     5.6  
     5.7 -val tacpbl = ref
     5.8 +val tacpbl = Unsynchronized.ref
     5.9    (distinct (remove op = "" (!tacs (*@ !subpbls*))));
    5.10  (*--^^^----- SHIFT? or delete ?*)
    5.11  

     6.1 --- a/src/Tools/isac/calcelems.sml	Mon Sep 13 17:21:22 2010 +0200
     6.2 +++ b/src/Tools/isac/calcelems.sml	Mon Sep 13 18:12:15 2010 +0200
     6.3 @@ -346,8 +346,9 @@
     6.4  (*rewrite orders, also stored in 'type met' and type 'and rls'
     6.5    The association list is required for 'rewrite.."rew_ord"..'
     6.6    WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
     6.7 -val rew_ord' = 
     6.8 -    ref ([]:(rew_ord' *        (*the key for the association list         *)
     6.9 +val rew_ord' =
    6.10 +    Unsynchronized.ref
    6.11 +        ([]:(rew_ord' *        (*the key for the association list         *)
    6.12  	     (subst 	       (*the bound variables - they get high order*)
    6.13  	      -> (term * term) (*(t1, t2) to be compared                  *)
    6.14  	      -> bool))        (*if t1 <= t2 then true else false         *)