# HG changeset patch
# User wenzelm
# Date 1183494445 -7200
# Node ID 0de52773029493ecedcf1f17b56da3b076d25c4a
# Parent  9325845aff1c6795680146876dcb1d00e4d2062d
tuned;

diff -r 9325845aff1c -r 0de527730294 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jul 03 22:27:19 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jul 03 22:27:25 2007 +0200
@@ -21,7 +21,8 @@
 
 structure Normalizer: NORMALIZER = 
 struct
-open Misc;
+
+open Conv Misc;
 
 local
  val pls_const = @{cterm "Numeral.Pls"}
diff -r 9325845aff1c -r 0de527730294 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Tue Jul 03 22:27:19 2007 +0200
+++ b/src/Pure/General/basics.ML	Tue Jul 03 22:27:25 2007 +0200
@@ -81,13 +81,13 @@
   | the NONE = raise Option;
 
 fun these (SOME x) = x
-  | these _ = [];
+  | these NONE = [];
 
 fun the_list (SOME x) = [x]
-  | the_list _ = []
+  | the_list NONE = []
 
 fun the_default x (SOME y) = y
-  | the_default x _ = x;
+  | the_default x NONE = x;
 
 fun perhaps f x = the_default x (f x);