1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -467,7 +467,7 @@
     1.4         scr = Script ((term_of o the o (parse thy)) "empty_script")
     1.5         }:rls);
     1.6  
     1.7 -ruleset' := overwritelthy thy (!ruleset',
     1.8 +ruleset' := overwritelthy @{theory} (!ruleset',
     1.9  		[("cancel_leading_coeff",cancel_leading_coeff),
    1.10  		 ("complete_square",complete_square),
    1.11  		 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
    1.12 @@ -806,7 +806,7 @@
    1.13        }:rls);
    1.14    
    1.15  ruleset' := 
    1.16 -overwritelthy thy 
    1.17 +overwritelthy @{theory} 
    1.18                (!ruleset',
    1.19                 [("d0_polyeq_simplify", d0_polyeq_simplify),
    1.20                  ("d1_polyeq_simplify", d1_polyeq_simplify),
    1.21 @@ -1439,7 +1439,7 @@
    1.22        scr = EmptyScr}:rls);      
    1.23  
    1.24  
    1.25 -ruleset' := overwritelthy thy (!ruleset',
    1.26 +ruleset' := overwritelthy @{theory} (!ruleset',
    1.27    [("order_add_mult_in", order_add_mult_in),
    1.28     ("collect_bdv", collect_bdv),
    1.29     ("make_polynomial_in", make_polynomial_in),