diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Apr 13 15:14:15 2019 +0200
+++ b/src/HOL/Tools/groebner.ML	Sat Apr 13 16:26:19 2019 +0200
@@ -481,7 +481,7 @@
   \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
    let
     val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
-    val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
+    val T = Thm.dest_ctyp_nth 0 (Thm.ctyp_of_cterm p)
     val th0 = Conv.fconv_rule (Thm.beta_conversion true)
         (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
     val pv = (Thm.rhs_of o Thm.beta_conversion true)