--- a/src/Pure/Isar/obtain.ML Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Apr 27 21:50:04 2011 +0200
@@ -196,7 +196,7 @@
val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
- val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
+ val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
val (prems, ctxt'') =
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
(Drule.strip_imp_prems stmt) fix_ctxt;