# HG changeset patch
# User wenzelm
# Date 1183586779 -7200
# Node ID 297c6d706322f27344d6781abf4766f034aeadc6
# Parent  998a6fda9bb6c3d711a8998dcbf119c86d540b76
tuned;

diff -r 998a6fda9bb6 -r 297c6d706322 src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Jul 05 00:06:18 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Jul 05 00:06:19 2007 +0200
@@ -8,7 +8,7 @@
 signature NORMALIZER_DATA =
 sig
   type entry
-  val get: Proof.context -> simpset * ((thm * entry) list)
+  val get: Proof.context -> simpset * (thm * entry) list
   val match: Proof.context -> cterm -> entry option
   val del: attribute
   val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
@@ -41,11 +41,11 @@
 
 structure Data = GenericDataFun
 (
-  type T = simpset * ((thm * entry) list);
+  type T = simpset * (thm * entry) list;
   val empty = (HOL_basic_ss, []);
   val extend = I;
-  fun merge _ ((ss, e), (ss', e')) = (merge_ss (ss, ss'), 
-                                      AList.merge eq_key (K true) (e,e'));
+  fun merge _ ((ss, e), (ss', e')) =
+    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
 );
 
 val get = Data.get o Context.Proof;
@@ -134,7 +134,6 @@
       val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
 
       val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
-      val _ = map print_thm sr_rules';
       val semiring = (sr_ops, sr_rules');
       val ring = (r_ops, r_rules');
     in
diff -r 998a6fda9bb6 -r 297c6d706322 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Thu Jul 05 00:06:18 2007 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Thu Jul 05 00:06:19 2007 +0200
@@ -46,9 +46,10 @@
 theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
   by algebra
 
-lemma fixes x::"'a::{idom,recpower,number_ring}"
-shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
-by algebra
+lemma
+  fixes x::"'a::{idom,recpower,number_ring}"
+  shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
+  by algebra
 
 subsection {* Lemmas for Lagrange's theorem *}