--- 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"}
--- 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);