diff -r 17909568216e -r 57df8a85317a src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Aug 20 11:01:05 2019 +0200
@@ -10,7 +10,7 @@
     (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
     conv ->  conv ->
      {ring_conv: Proof.context -> conv,
-     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
+     simple_ideal: cterm list -> cterm -> cterm ord -> cterm list,
      multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
      poly_eq_ss: simpset, unwind_conv: Proof.context -> conv}
   val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic