--- 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);