# HG changeset patch
# User wenzelm
# Date 1555185084 -7200
# Node ID a3d5e561e18a3be10c976b410fa0db1d058754bc
# Parent  62b19f19350af93310fc602b589d673fcc43fd5d
prefer ctyp operations;

diff -r 62b19f19350a -r a3d5e561e18a src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sat Apr 13 21:43:41 2019 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sat Apr 13 21:51:24 2019 +0200
@@ -41,9 +41,10 @@
     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
   | Const(\<^const_name>\<open>Ex\<close>,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
-  | Const(\<^const_name>\<open>All\<close>, allT)$_ =>
+  | Const(\<^const_name>\<open>All\<close>, _)$_ =>
     let
-     val T = Thm.ctyp_of ctxt (#1 (Term.dest_funT (#1 (Term.dest_funT allT))))
+     val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
+     val T = Thm.dest_ctyp_nth 0 (Thm.dest_ctyp_nth 0 allT)
      val p = Thm.dest_arg p
      val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
     in Thm.transitive th (conv env (Thm.rhs_of th))