1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 16:36:14 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 17:21:22 2010 +0200
1.3 @@ -260,7 +260,7 @@
1.4 raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
1.5 | uv_mod_pdiv p1 [x] =
1.6 let
1.7 - val xs=ref [];
1.8 + val xs= Unsynchronized.ref [];
1.9 in
1.10 if x<>0 then
1.11 (
1.12 @@ -273,13 +273,13 @@
1.13 | uv_mod_pdiv p1 p2 =
1.14 let
1.15 val n= uv_mod_deg(p2);
1.16 - val m= ref (uv_mod_deg(p1));
1.17 - val p1'=ref (rev(p1));
1.18 + val m= Unsynchronized.ref (uv_mod_deg(p1));
1.19 + val p1'= Unsynchronized.ref (rev(p1));
1.20 val p2'=(rev(p2));
1.21 val lc2=hd(p2');
1.22 - val q=ref [];
1.23 - val c=ref 0;
1.24 - val output=ref ([],[]);
1.25 + val q= Unsynchronized.ref [];
1.26 + val c= Unsynchronized.ref 0;
1.27 + val output= Unsynchronized.ref ([],[]);
1.28 in
1.29 (
1.30 if (!m)=0 orelse p2=[0]
1.31 @@ -314,13 +314,13 @@
1.32 fun uv_mod_pdivp (p1:uv_poly) (p2:uv_poly) p =
1.33 let
1.34 val n=uv_mod_deg(p2);
1.35 - val m=ref (uv_mod_deg(uv_mod_list_modp p1 p));
1.36 - val p1'=ref (rev(p1));
1.37 + val m= Unsynchronized.ref (uv_mod_deg(uv_mod_list_modp p1 p));
1.38 + val p1'= Unsynchronized.ref (rev(p1));
1.39 val p2'=(rev(uv_mod_list_modp p2 p));
1.40 val lc2=hd(p2');
1.41 - val q=ref [];
1.42 - val c=ref 0;
1.43 - val output=ref ([],[]);
1.44 + val q= Unsynchronized.ref [];
1.45 + val c= Unsynchronized.ref 0;
1.46 + val output= Unsynchronized.ref ([],[]);
1.47 in
1.48 (
1.49 if (!m)=0 orelse p2=[0] then raise error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
1.50 @@ -376,7 +376,7 @@
1.51 fun uv_mod_pp ([]:uv_poly) = []:uv_poly
1.52 | uv_mod_pp p =
1.53 let
1.54 - val c=ref 0;
1.55 + val c= Unsynchronized.ref 0;
1.56 in
1.57 (
1.58 c:=uv_mod_cont(p);
1.59 @@ -393,9 +393,9 @@
1.60 (*. calculates the euklidean polynomial remainder sequence in Zp .*)
1.61 fun uv_mod_prs_euklid_p(p1:uv_poly,p2:uv_poly,p)=
1.62 let
1.63 - val f =ref [];
1.64 - val f'=ref p2;
1.65 - val fi=ref [];
1.66 + val f = Unsynchronized.ref [];
1.67 + val f'= Unsynchronized.ref p2;
1.68 + val fi= Unsynchronized.ref [];
1.69 in
1.70 (
1.71 f:=p2::p1::[];
1.72 @@ -419,12 +419,12 @@
1.73 | uv_mod_gcd_modp p1 [] p= p1
1.74 | uv_mod_gcd_modp p1 p2 p=
1.75 let
1.76 - val p1'=ref[];
1.77 - val p2'=ref[];
1.78 - val pc=ref[];
1.79 - val g=ref [];
1.80 - val d=ref 0;
1.81 - val prs=ref [];
1.82 + val p1'= Unsynchronized.ref [];
1.83 + val p2'= Unsynchronized.ref [];
1.84 + val pc= Unsynchronized.ref [];
1.85 + val g= Unsynchronized.ref [];
1.86 + val d= Unsynchronized.ref 0;
1.87 + val prs= Unsynchronized.ref [];
1.88 in
1.89 (
1.90 if uv_mod_deg(p1)>=uv_mod_deg(p2) then
1.91 @@ -480,9 +480,9 @@
1.92 (*. gets the first prime, which is greater than p and does not divide g .*)
1.93 fun uv_mod_nextprime(g,p)=
1.94 let
1.95 - val list=ref [2];
1.96 - val exit=ref 0;
1.97 - val i = ref 2
1.98 + val list= Unsynchronized.ref [2];
1.99 + val exit= Unsynchronized.ref 0;
1.100 + val i = Unsynchronized.ref 2
1.101 in
1.102 while (!i<p) do (* calculates the primes lower then p *)
1.103 (
1.104 @@ -527,10 +527,10 @@
1.105 (*. chinese remainder algorithm .*)
1.106 fun uv_mod_cra2(r1,r2,m1,m2)=
1.107 let
1.108 - val c=ref 0;
1.109 - val r1'=ref 0;
1.110 - val d=ref 0;
1.111 - val a=ref 0;
1.112 + val c= Unsynchronized.ref 0;
1.113 + val r1'= Unsynchronized.ref 0;
1.114 + val d= Unsynchronized.ref 0;
1.115 + val a= Unsynchronized.ref 0;
1.116 in
1.117 (
1.118 while (uv_mod_mod2((!c)*m1,m2))<>1 do
1.119 @@ -552,20 +552,20 @@
1.120 (*. calculates the gcd of two uv polynomials p1' and p2' with the modular algorithm .*)
1.121 fun uv_mod_gcd (p1':uv_poly) (p2':uv_poly) =
1.122 let
1.123 - val p1=ref (uv_mod_pp(p1'));
1.124 - val p2=ref (uv_mod_pp(p2'));
1.125 + val p1= Unsynchronized.ref (uv_mod_pp(p1'));
1.126 + val p2= Unsynchronized.ref (uv_mod_pp(p2'));
1.127 val c=gcd_int (uv_mod_cont(p1')) (uv_mod_cont(p2'));
1.128 - val temp=ref [];
1.129 - val cp=ref [];
1.130 - val qp=ref [];
1.131 - val q=ref[];
1.132 - val pn=ref 0;
1.133 - val d=ref 0;
1.134 - val g1=ref 0;
1.135 - val p=ref 0;
1.136 - val m=ref 0;
1.137 - val exit=ref 0;
1.138 - val i=ref 1;
1.139 + val temp= Unsynchronized.ref [];
1.140 + val cp= Unsynchronized.ref [];
1.141 + val qp= Unsynchronized.ref [];
1.142 + val q= Unsynchronized.ref [];
1.143 + val pn= Unsynchronized.ref 0;
1.144 + val d= Unsynchronized.ref 0;
1.145 + val g1= Unsynchronized.ref 0;
1.146 + val p= Unsynchronized.ref 0;
1.147 + val m= Unsynchronized.ref 0;
1.148 + val exit= Unsynchronized.ref 0;
1.149 + val i= Unsynchronized.ref 1;
1.150 in
1.151 if length(!p1)>length(!p2) then ()
1.152 else
1.153 @@ -705,7 +705,7 @@
1.154 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)
1.155 fun mv_geq order ((x1,x):mv_monom,(x2,y):mv_monom) =
1.156 let
1.157 - val temp=ref EQUAL;
1.158 + val temp= Unsynchronized.ref EQUAL;
1.159 in
1.160 if order=LEX_ then
1.161 (
1.162 @@ -765,9 +765,9 @@
1.163 | mv_lc([(x,y)],order) = mv_rev_to(mv_cut(mv_rev_to([(x,y)])))
1.164 | mv_lc(p1,order) =
1.165 let
1.166 - val p1o=ref (rev(sort (mv_geq order) (mv_rev_to(p1))));
1.167 + val p1o= Unsynchronized.ref (rev(sort (mv_geq order) (mv_rev_to(p1))));
1.168 val lp=hd(#2(hd(!p1o)));
1.169 - val lc=ref [];
1.170 + val lc= Unsynchronized.ref [];
1.171 in
1.172 (
1.173 while (length(!p1o)>0 andalso hd(#2(hd(!p1o)))=lp) do
1.174 @@ -851,8 +851,8 @@
1.175 | mv_mdiv(_,(0,[]))= raise error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
1.176 | mv_mdiv(p1:mv_monom,p2:mv_monom)=
1.177 let
1.178 - val c=ref (#1(p2));
1.179 - val pp=ref [];
1.180 + val c= Unsynchronized.ref (#1(p2));
1.181 + val pp= Unsynchronized.ref [];
1.182 in
1.183 (
1.184 if !c=0 then raise error("MV_MDIV_EXCEPTION Dividing by zero")
1.185 @@ -878,12 +878,12 @@
1.186 | mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
1.187 | mv_division(f,g,order)=
1.188 let
1.189 - val r=ref [];
1.190 - val q=ref [];
1.191 - val g'=ref [];
1.192 - val k=ref 0;
1.193 - val m=ref (0,[0]);
1.194 - val exit=ref 0;
1.195 + val r= Unsynchronized.ref [];
1.196 + val q= Unsynchronized.ref [];
1.197 + val g'= Unsynchronized.ref ([] : mv_monom list);
1.198 + val k= Unsynchronized.ref 0;
1.199 + val m= Unsynchronized.ref (0,[0]);
1.200 + val exit= Unsynchronized.ref 0;
1.201 in
1.202 r := rev(sort (mv_geq order) (mv_shorten(f,order)));
1.203 g':= rev(sort (mv_geq order) (mv_shorten(g,order)));
1.204 @@ -959,10 +959,10 @@
1.205 fun uv_to_list ([]:mv_poly)=[]:uv_poly
1.206 | uv_to_list ((c1,e1)::others) =
1.207 let
1.208 - val count=ref 0;
1.209 + val count= Unsynchronized.ref 0;
1.210 val max=mv_grad((c1,e1)::others);
1.211 - val help=ref ((c1,e1)::others);
1.212 - val list=ref [];
1.213 + val help= Unsynchronized.ref ((c1,e1)::others);
1.214 + val list= Unsynchronized.ref [];
1.215 in
1.216 if length(e1)>1 then raise error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
1.217 else if length(e1)=0 then [c1]
1.218 @@ -990,9 +990,9 @@
1.219 fun uv_to_poly ([]:uv_poly) = []:mv_poly
1.220 | uv_to_poly p1 =
1.221 let
1.222 - val count=ref 0;
1.223 - val help=ref p1;
1.224 - val list=ref [];
1.225 + val count= Unsynchronized.ref 0;
1.226 + val help= Unsynchronized.ref p1;
1.227 + val list= Unsynchronized.ref [];
1.228 in
1.229 while length(!help)>0 do
1.230 (
1.231 @@ -1009,14 +1009,14 @@
1.232 | uv_gcd p1 ([]:mv_poly) = p1
1.233 | uv_gcd p1 [(c,[e])] =
1.234 let
1.235 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
1.236 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
1.237 val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));
1.238 in
1.239 [(gcd_int (uv_content2(p1)) c,[min])]
1.240 end
1.241 | uv_gcd [(c,[e])] p2 =
1.242 let
1.243 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p2,LEX_))));
1.244 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p2,LEX_))));
1.245 val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));
1.246 in
1.247 [(gcd_int (uv_content2(p2)) c,[min])]
1.248 @@ -1027,11 +1027,11 @@
1.249 fun mv_newton_help ([]:mv_poly list,k:int) = []:mv_poly list
1.250 | mv_newton_help (pl:mv_poly list,k) =
1.251 let
1.252 - val x=ref (rev(pl));
1.253 - val t=ref [];
1.254 - val y=ref [];
1.255 - val n=ref 1;
1.256 - val n1=ref[];
1.257 + val x= Unsynchronized.ref (rev(pl));
1.258 + val t= Unsynchronized.ref [];
1.259 + val y= Unsynchronized.ref [];
1.260 + val n= Unsynchronized.ref 1;
1.261 + val n1= Unsynchronized.ref [];
1.262 in
1.263 (
1.264 while length(!x)>1 do
1.265 @@ -1052,8 +1052,8 @@
1.266 | mv_newton_add [x:mv_poly] t = x
1.267 | mv_newton_add (pl:mv_poly list) t =
1.268 let
1.269 - val expos=ref [];
1.270 - val pll=ref pl;
1.271 + val expos= Unsynchronized.ref [];
1.272 + val pll= Unsynchronized.ref pl;
1.273 in
1.274 (
1.275
1.276 @@ -1079,12 +1079,12 @@
1.277 | mv_newton ([mp]:(mv_poly) list) = mp:mv_poly
1.278 | mv_newton pl =
1.279 let
1.280 - val c=ref pl;
1.281 - val c1=ref [];
1.282 + val c= Unsynchronized.ref pl;
1.283 + val c1= Unsynchronized.ref [];
1.284 val n=length(pl);
1.285 - val k=ref 1;
1.286 - val i=ref n;
1.287 - val ppl=ref [];
1.288 + val k= Unsynchronized.ref 1;
1.289 + val i= Unsynchronized.ref n;
1.290 + val ppl= Unsynchronized.ref [];
1.291 in
1.292 c1:=hd(pl)::[];
1.293 c:=mv_newton_help(!c,!k);
1.294 @@ -1111,8 +1111,8 @@
1.295 fun mv_min_pp([]:mv_poly)=[]
1.296 | mv_min_pp((c,e)::xs)=
1.297 let
1.298 - val y=ref xs;
1.299 - val x=ref [];
1.300 + val y= Unsynchronized.ref xs;
1.301 + val x= Unsynchronized.ref [];
1.302 in
1.303 (
1.304 x:=e;
1.305 @@ -1136,9 +1136,9 @@
1.306 fun mv_content([]:mv_poly) = []:mv_poly
1.307 | mv_content(p1) =
1.308 let
1.309 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
1.310 - val test=ref (hd(#2(hd(!list))));
1.311 - val result=ref [];
1.312 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
1.313 + val test= Unsynchronized.ref (hd(#2(hd(!list))));
1.314 + val result= Unsynchronized.ref [];
1.315 val min=(hd(#2(hd(rev(!list)))));
1.316 in
1.317 (
1.318 @@ -1170,8 +1170,8 @@
1.319 (*. calculates the primitiv part of a polynomial .*)
1.320 and mv_pp([]:mv_poly) = []:mv_poly
1.321 | mv_pp(p1) = let
1.322 - val cont=ref [];
1.323 - val pp=ref[];
1.324 + val cont= Unsynchronized.ref [];
1.325 + val pp= Unsynchronized.ref [];
1.326 in
1.327 cont:=mv_content(p1);
1.328 pp:=(#1(mv_division(p1,!cont,LEX_)));
1.329 @@ -1215,20 +1215,20 @@
1.330 );
1.331 val p1= #1(mv_division(p1',mv_content(p1'),LEX_));
1.332 val p2= #1(mv_division(p2',mv_content(p2'),LEX_));
1.333 - val gcd=ref [];
1.334 - val candidate=ref [];
1.335 - val interpolation_list=ref [];
1.336 - val delta=ref [];
1.337 - val p1r = ref [];
1.338 - val p2r = ref [];
1.339 - val p1r' = ref [];
1.340 - val p2r' = ref [];
1.341 - val factor=ref [];
1.342 - val r=ref 0;
1.343 - val gcd_r=ref [];
1.344 - val d=ref 0;
1.345 - val exit=ref 0;
1.346 - val current_degree=ref 99999; (*. FIXME: unlimited ! .*)
1.347 + val gcd= Unsynchronized.ref [];
1.348 + val candidate= Unsynchronized.ref [];
1.349 + val interpolation_list= Unsynchronized.ref [];
1.350 + val delta= Unsynchronized.ref [];
1.351 + val p1r = Unsynchronized.ref [];
1.352 + val p2r = Unsynchronized.ref [];
1.353 + val p1r' = Unsynchronized.ref [];
1.354 + val p2r' = Unsynchronized.ref [];
1.355 + val factor= Unsynchronized.ref [];
1.356 + val r= Unsynchronized.ref 0;
1.357 + val gcd_r= Unsynchronized.ref [];
1.358 + val d= Unsynchronized.ref 0;
1.359 + val exit= Unsynchronized.ref 0;
1.360 + val current_degree= Unsynchronized.ref 99999; (*. FIXME: unlimited ! .*)
1.361 in
1.362 (
1.363 if vc<2 then (* areUnivariate(p1',p2') *)
1.364 @@ -1349,11 +1349,11 @@
1.365 converts the term to a list of coefficients .*)
1.366 fun term2coef' (t as Free(str,_(*typ*))) v :mv_poly option =
1.367 let
1.368 - val x=ref NONE;
1.369 - val len=ref 0;
1.370 - val vl=ref [];
1.371 - val vh=ref [];
1.372 - val i=ref 0;
1.373 + val x= Unsynchronized.ref NONE;
1.374 + val len= Unsynchronized.ref 0;
1.375 + val vl= Unsynchronized.ref [];
1.376 + val vh= Unsynchronized.ref [];
1.377 + val i= Unsynchronized.ref 0;
1.378 in
1.379 if is_numeral str then
1.380 (
1.381 @@ -1381,10 +1381,10 @@
1.382 end
1.383 | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
1.384 let
1.385 - val t1pp=ref [];
1.386 - val t2pp=ref [];
1.387 - val t1c=ref 0;
1.388 - val t2c=ref 0;
1.389 + val t1pp= Unsynchronized.ref [];
1.390 + val t2pp= Unsynchronized.ref [];
1.391 + val t1c= Unsynchronized.ref 0;
1.392 + val t2c= Unsynchronized.ref 0;
1.393 in
1.394 (
1.395 t1pp:=(#2(hd(the(term2coef' t1 v))));
1.396 @@ -1398,12 +1398,12 @@
1.397 end
1.398 | term2coef' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $ (t2 as Free (str2,_))) v :mv_poly option=
1.399 let
1.400 - val x=ref NONE;
1.401 - val len=ref 0;
1.402 - val vl=ref [];
1.403 - val vh=ref [];
1.404 - val vtemp=ref [];
1.405 - val i=ref 0;
1.406 + val x= Unsynchronized.ref NONE;
1.407 + val len= Unsynchronized.ref 0;
1.408 + val vl= Unsynchronized.ref [];
1.409 + val vh= Unsynchronized.ref [];
1.410 + val vtemp= Unsynchronized.ref [];
1.411 + val i= Unsynchronized.ref 0;
1.412 in
1.413 (
1.414 if (not o is_numeral) str1 andalso is_numeral str2 then
1.415 @@ -1462,11 +1462,11 @@
1.416
1.417 | term2poly' (Free(str,_)) v :mv_poly option =
1.418 let
1.419 - val x=ref NONE;
1.420 - val len=ref 0;
1.421 - val vl=ref [];
1.422 - val vh=ref [];
1.423 - val i=ref 0;
1.424 + val x= Unsynchronized.ref NONE;
1.425 + val len= Unsynchronized.ref 0;
1.426 + val vl= Unsynchronized.ref [];
1.427 + val vh= Unsynchronized.ref [];
1.428 + val i= Unsynchronized.ref 0;
1.429 in
1.430 if is_numeral str then
1.431 (
1.432 @@ -1494,10 +1494,10 @@
1.433 end
1.434 | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
1.435 let
1.436 - val t1pp=ref [];
1.437 - val t2pp=ref [];
1.438 - val t1c=ref 0;
1.439 - val t2c=ref 0;
1.440 + val t1pp= Unsynchronized.ref [];
1.441 + val t2pp= Unsynchronized.ref [];
1.442 + val t1c= Unsynchronized.ref 0;
1.443 + val t2c= Unsynchronized.ref 0;
1.444 in
1.445 (
1.446 t1pp:=(#2(hd(the(term2poly' t1 v))));
1.447 @@ -1513,12 +1513,12 @@
1.448 | term2poly' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $
1.449 (t2 as Free (str2,_))) v :mv_poly option=
1.450 let
1.451 - val x=ref NONE;
1.452 - val len=ref 0;
1.453 - val vl=ref [];
1.454 - val vh=ref [];
1.455 - val vtemp=ref [];
1.456 - val i=ref 0;
1.457 + val x= Unsynchronized.ref NONE;
1.458 + val len= Unsynchronized.ref 0;
1.459 + val vl= Unsynchronized.ref [];
1.460 + val vh= Unsynchronized.ref [];
1.461 + val vtemp= Unsynchronized.ref [];
1.462 + val i= Unsynchronized.ref 0;
1.463 in
1.464 (
1.465 if (not o is_numeral) str1 andalso is_numeral str2 then
1.466 @@ -1580,8 +1580,8 @@
1.467 (*. converts a powerproduct into term representation .*)
1.468 fun powerproduct2term(xs,v) =
1.469 let
1.470 - val xss=ref xs;
1.471 - val vv=ref v;
1.472 + val xss= Unsynchronized.ref xs;
1.473 + val vv= Unsynchronized.ref v;
1.474 in
1.475 (
1.476 while hd(!xss)=0 do
1.477 @@ -1745,9 +1745,9 @@
1.478 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)
1.479 fun step_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
1.480 let
1.481 - val p1' = ref [];
1.482 - val p2' = ref [];
1.483 - val p3 = ref []
1.484 + val p1' = Unsynchronized.ref [];
1.485 + val p2' = Unsynchronized.ref [];
1.486 + val p3 = Unsynchronized.ref []
1.487 val vars = rev(get_vars(p1) union get_vars(p2));
1.488 in
1.489 (
1.490 @@ -1810,9 +1810,9 @@
1.491 (*. same as step_cancel, this time for expanded forms (input+output) .*)
1.492 fun step_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
1.493 let
1.494 - val p1' = ref [];
1.495 - val p2' = ref [];
1.496 - val p3 = ref []
1.497 + val p1' = Unsynchronized.ref [];
1.498 + val p2' = Unsynchronized.ref [];
1.499 + val p3 = Unsynchronized.ref []
1.500 val vars = rev(get_vars(p1) union get_vars(p2));
1.501 in
1.502 (
1.503 @@ -1874,9 +1874,9 @@
1.504 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
1.505 fun direct_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
1.506 let
1.507 - val p1' = ref [];
1.508 - val p2' = ref [];
1.509 - val p3 = ref []
1.510 + val p1' = Unsynchronized.ref [];
1.511 + val p2' = Unsynchronized.ref [];
1.512 + val p3 = Unsynchronized.ref []
1.513 val vars = rev(get_vars(p1) union get_vars(p2));
1.514 in
1.515 (
1.516 @@ -1959,9 +1959,9 @@
1.517 (*. same es direct_cancel, this time for expanded forms (input+output).*)
1.518 fun direct_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
1.519 let
1.520 - val p1' = ref [];
1.521 - val p2' = ref [];
1.522 - val p3 = ref []
1.523 + val p1' = Unsynchronized.ref [];
1.524 + val p2' = Unsynchronized.ref [];
1.525 + val p3 = Unsynchronized.ref []
1.526 val vars = rev(get_vars(p1) union get_vars(p2));
1.527 in
1.528 (
1.529 @@ -2046,18 +2046,18 @@
1.530 fun add_fract ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
1.531 let
1.532 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
1.533 - val t11'=ref (the(term2poly t11 vars));
1.534 + val t11'= Unsynchronized.ref (the(term2poly t11 vars));
1.535 val _= writeln"### add_fract: done t11"
1.536 - val t12'=ref (the(term2poly t12 vars));
1.537 + val t12'= Unsynchronized.ref (the(term2poly t12 vars));
1.538 val _= writeln"### add_fract: done t12"
1.539 - val t21'=ref (the(term2poly t21 vars));
1.540 + val t21'= Unsynchronized.ref (the(term2poly t21 vars));
1.541 val _= writeln"### add_fract: done t21"
1.542 - val t22'=ref (the(term2poly t22 vars));
1.543 + val t22'= Unsynchronized.ref (the(term2poly t22 vars));
1.544 val _= writeln"### add_fract: done t22"
1.545 - val den=ref [];
1.546 - val nom=ref [];
1.547 - val m1=ref [];
1.548 - val m2=ref [];
1.549 + val den= Unsynchronized.ref [];
1.550 + val nom= Unsynchronized.ref [];
1.551 + val m1= Unsynchronized.ref [];
1.552 + val m2= Unsynchronized.ref [];
1.553 in
1.554
1.555 (
1.556 @@ -2092,14 +2092,14 @@
1.557 fun add_fract_exp ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
1.558 let
1.559 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
1.560 - val t11'=ref (the(expanded2poly t11 vars));
1.561 - val t12'=ref (the(expanded2poly t12 vars));
1.562 - val t21'=ref (the(expanded2poly t21 vars));
1.563 - val t22'=ref (the(expanded2poly t22 vars));
1.564 - val den=ref [];
1.565 - val nom=ref [];
1.566 - val m1=ref [];
1.567 - val m2=ref [];
1.568 + val t11'= Unsynchronized.ref (the(expanded2poly t11 vars));
1.569 + val t12'= Unsynchronized.ref (the(expanded2poly t12 vars));
1.570 + val t21'= Unsynchronized.ref (the(expanded2poly t21 vars));
1.571 + val t22'= Unsynchronized.ref (the(expanded2poly t22 vars));
1.572 + val den= Unsynchronized.ref [];
1.573 + val nom= Unsynchronized.ref [];
1.574 + val m1= Unsynchronized.ref [];
1.575 + val m2= Unsynchronized.ref [];
1.576 in
1.577
1.578 (
1.579 @@ -2176,8 +2176,8 @@
1.580 fun termlist2denominators [] = ([],[])
1.581 | termlist2denominators xs =
1.582 let
1.583 - val xxs=ref xs;
1.584 - val var=ref [];
1.585 + val xxs= Unsynchronized.ref xs;
1.586 + val var= Unsynchronized.ref [];
1.587 in
1.588 var:=[];
1.589 while length(!xxs)>0 do
1.590 @@ -2210,8 +2210,8 @@
1.591 fun termlist2denominators [] = ([],[])
1.592 | termlist2denominators xs =
1.593 let
1.594 - val xxs=ref xs;
1.595 - val var=ref [];
1.596 + val xxs= Unsynchronized.ref xs;
1.597 + val var= Unsynchronized.ref [];
1.598 in
1.599 var:=[];
1.600 while length(!xxs)>0 do
1.601 @@ -2232,8 +2232,8 @@
1.602 fun termlist2denominators_exp [] = ([],[])
1.603 | termlist2denominators_exp xs =
1.604 let
1.605 - val xxs=ref xs;
1.606 - val var=ref [];
1.607 + val xxs= Unsynchronized.ref xs;
1.608 + val var= Unsynchronized.ref [];
1.609 in
1.610 var:=[];
1.611 while length(!xxs)>0 do