1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -384,7 +384,7 @@
     1.4  		];
     1.5  
     1.6  ruleset' := 
     1.7 -overwritelthy thy (!ruleset',
     1.8 +overwritelthy @{theory} (!ruleset',
     1.9  		   [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
    1.10  		    ("fasse_zusammen", prep_rls fasse_zusammen),
    1.11  		    ("verschoenere", prep_rls verschoenere),
    1.12 @@ -404,7 +404,7 @@
    1.13  store_pbt
    1.14   (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_minus" [] e_pblID
    1.15   (["plus_minus","polynom","vereinfachen"],
    1.16 -  [("#Given" ,["term t_"]),
    1.17 +  [("#Given" ,["TERM t_"]),
    1.18     ("#Where" ,["t_ is_polyexp",
    1.19  	       "Not (matchsub (?a + (?b + ?c)) t_ | " ^
    1.20  	       "     matchsub (?a + (?b - ?c)) t_ | " ^
    1.21 @@ -433,7 +433,7 @@
    1.22  store_pbt
    1.23   (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer" [] e_pblID
    1.24   (["klammer","polynom","vereinfachen"],
    1.25 -  [("#Given" ,["term t_"]),
    1.26 +  [("#Given" ,["TERM t_"]),
    1.27     ("#Where" ,["t_ is_polyexp",
    1.28  	       "Not (matchsub (?a * (?b + ?c)) t_ | " ^
    1.29  	       "     matchsub (?a * (?b - ?c)) t_ | " ^
    1.30 @@ -457,7 +457,7 @@
    1.31  store_pbt
    1.32   (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer_mal" [] e_pblID
    1.33   (["binom_klammer","polynom","vereinfachen"],
    1.34 -  [("#Given" ,["term t_"]),
    1.35 +  [("#Given" ,["TERM t_"]),
    1.36     ("#Where" ,["t_ is_polyexp"]),
    1.37     ("#Find"  ,["normalform n_"])
    1.38    ],
    1.39 @@ -503,7 +503,7 @@
    1.40  store_met
    1.41      (prep_met (theory "PolyMinus") "met_simp_poly_minus" [] e_metID
    1.42  	      (["simplification","for_polynomials","with_minus"],
    1.43 -	       [("#Given" ,["term t_"]),
    1.44 +	       [("#Given" ,["TERM t_"]),
    1.45  		("#Where" ,["t_ is_polyexp",
    1.46  	       "Not (matchsub (?a + (?b + ?c)) t_ | " ^
    1.47  	       "     matchsub (?a + (?b - ?c)) t_ | " ^
    1.48 @@ -533,7 +533,7 @@
    1.49  store_met
    1.50      (prep_met (theory "PolyMinus") "met_simp_poly_parenth" [] e_metID
    1.51  	      (["simplification","for_polynomials","with_parentheses"],
    1.52 -	       [("#Given" ,["term t_"]),
    1.53 +	       [("#Given" ,["TERM t_"]),
    1.54  		("#Where" ,["t_ is_polyexp"]),
    1.55  		("#Find"  ,["normalform n_"])
    1.56  		],
    1.57 @@ -552,7 +552,7 @@
    1.58  store_met
    1.59      (prep_met (theory "PolyMinus") "met_simp_poly_parenth_mult" [] e_metID
    1.60  	      (["simplification","for_polynomials","with_parentheses_mult"],
    1.61 -	       [("#Given" ,["term t_"]),
    1.62 +	       [("#Given" ,["TERM t_"]),
    1.63  		("#Where" ,["t_ is_polyexp"]),
    1.64  		("#Find"  ,["normalform n_"])
    1.65  		],