--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sun Jul 05 15:02:30 2015 +0200
@@ -625,7 +625,10 @@
val vs = frees_of ctxt (Thm.term_of ct)
val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
val vars_of = get_vars Term.add_vars Var (K true) ctxt'
- in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
+ in
+ (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm,
+ ctxt')
+ end
val sk_rules = @{lemma
"c = (SOME x. P x) ==> (EX x. P x) = P c"