src/HOL/Tools/Groebner_Basis/normalizer.ML
changeset 23559 0de527730294
parent 23485 881b04972953
child 23580 998a6fda9bb6
--- 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"}