diff -r 833abbc3e733 -r c642b36f2bec src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Oct 31 12:19:41 2007 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Oct 31 12:19:43 2007 +0100
@@ -20,9 +20,28 @@
 structure Normalizer: NORMALIZER = 
 struct
 
-open Conv Misc;
+open Conv;
 
 (* Very basic stuff for terms *)
+
+fun is_comb ct =
+  (case Thm.term_of ct of
+    _ $ _ => true
+  | _ => false);
+
+val concl = Thm.cprop_of #> Thm.dest_arg;
+
+fun is_binop ct ct' =
+  (case Thm.term_of ct' of
+    c $ _ $ _ => term_of ct aconv c
+  | _ => false);
+
+fun dest_binop ct ct' =
+  if is_binop ct ct' then Thm.dest_binop ct'
+  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
+
+fun inst_thm inst = Thm.instantiate ([], inst);
+
 val dest_numeral = term_of #> HOLogic.dest_number #> snd;
 val is_numeral = can dest_numeral;
 
@@ -593,7 +612,7 @@
                               addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
 
 fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
-fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom}, 
+fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
                                      {conv, dest_const, mk_const, is_const}) ord =
   let
     val pow_conv =