1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -64,10 +64,8 @@
     1.4  subsubsection {* Declaring the abstract theory *}
     1.5  
     1.6  lemma semiring_ops:
     1.7 -  fixes meta_term :: "'a => prop"  ("TERM _")
     1.8    shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
     1.9 -    and "TERM r0" and "TERM r1"
    1.10 -  by rule+
    1.11 +    and "TERM r0" and "TERM r1" .
    1.12  
    1.13  lemma semiring_rules:
    1.14    "add (mul a m) (mul b m) = mul (add a b) m"
    1.15 @@ -226,9 +224,7 @@
    1.16      and sub_add: "sub x y = add x (neg y)"
    1.17  begin
    1.18  
    1.19 -lemma ring_ops:
    1.20 -  fixes meta_term :: "'a => prop"  ("TERM _")
    1.21 -  shows "TERM (sub x y)" and "TERM (neg x)" .
    1.22 +lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
    1.23  
    1.24  lemmas ring_rules = neg_mul sub_add
    1.25