--- a/src/HOL/Tools/groebner.ML Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/groebner.ML Sat May 11 16:57:18 2013 +0200
@@ -864,7 +864,7 @@
val (vars,bod) = strip_exists tm
val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
val th1 = (the (get_first (try (isolate_variable vars)) cjs)
- handle Option => raise CTERM ("unwind_polys_conv",[tm]))
+ handle Option.Option => raise CTERM ("unwind_polys_conv",[tm]))
val eq = Thm.lhs_of th1
val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
val th2 = conj_ac_rule (mk_eq bod bod')