diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Nov 20 00:03:47 2008 +0100
@@ -64,10 +64,8 @@
 subsubsection {* Declaring the abstract theory *}
 
 lemma semiring_ops:
-  fixes meta_term :: "'a => prop"  ("TERM _")
   shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
-    and "TERM r0" and "TERM r1"
-  by rule+
+    and "TERM r0" and "TERM r1" .
 
 lemma semiring_rules:
   "add (mul a m) (mul b m) = mul (add a b) m"
@@ -226,9 +224,7 @@
     and sub_add: "sub x y = add x (neg y)"
 begin
 
-lemma ring_ops:
-  fixes meta_term :: "'a => prop"  ("TERM _")
-  shows "TERM (sub x y)" and "TERM (neg x)" .
+lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
 
 lemmas ring_rules = neg_mul sub_add