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