diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -496,7 +496,7 @@
 
 fun simple_choose v th =
    choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
-    ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
+    (Thm.dest_arg (hd (Thm.chyps_of th))))) th
 
 
  fun mkexi v th =