--- a/src/HOL/Library/positivstellensatz.ML Sat Apr 13 15:14:15 2019 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Sat Apr 13 16:26:19 2019 +0200
@@ -522,7 +522,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 = 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)