1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -3761,7 +3761,7 @@
     1.4  (* ------------------------------------------------------------------ *)
     1.5  
     1.6  
     1.7 -ruleset' := overwritelthy thy (!ruleset',
     1.8 +ruleset' := overwritelthy @{theory} (!ruleset',
     1.9    [("calculate_Rational", calculate_Rational),
    1.10     ("calc_rat_erls",calc_rat_erls),
    1.11     ("rational_erls", rational_erls),
    1.12 @@ -3794,7 +3794,7 @@
    1.13  store_pbt
    1.14   (prep_pbt (theory "Rational") "pbl_simp_rat" [] e_pblID
    1.15   (["rational","simplification"],
    1.16 -  [("#Given" ,["term t_"]),
    1.17 +  [("#Given" ,["TERM t_"]),
    1.18     ("#Where" ,["t_ is_ratpolyexp"]),
    1.19     ("#Find"  ,["normalform n_"])
    1.20    ],
    1.21 @@ -3809,7 +3809,7 @@
    1.22  store_met
    1.23      (prep_met (theory "Rational") "met_simp_rat" [] e_metID
    1.24  	      (["simplification","of_rationals"],
    1.25 -	       [("#Given" ,["term t_"]),
    1.26 +	       [("#Given" ,["TERM t_"]),
    1.27  		("#Where" ,["t_ is_ratpolyexp"]),
    1.28  		("#Find"  ,["normalform n_"])
    1.29  		],