# HG changeset patch
# User haftmann
# Date 1579720678 0
# Node ID fb9edfe035e1559226f0f7bb8c029f5b3be1305d
# Parent  a3ae93ed7b1b4822c4b8466bee479736b930e9b8
tuned

diff -r a3ae93ed7b1b -r fb9edfe035e1 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Jan 22 19:17:57 2020 +0000
+++ b/src/Provers/hypsubst.ML	Wed Jan 22 19:17:58 2020 +0000
@@ -171,8 +171,8 @@
         val U = Term.fastype_of1 (rev (map snd ps), t);
         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
         val rl' = Thm.lift_rule cBi rl;
-        val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
-          (Logic.strip_assums_concl (Thm.prop_of rl')));
+        val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop
+          (Logic.strip_assums_concl (Thm.prop_of rl'))));
         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
         val (Ts, V) = split_last (Term.binder_types T);