--- a/src/Pure/goal.ML Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/goal.ML Wed Jul 08 19:28:43 2015 +0200
@@ -328,7 +328,7 @@
fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
let
- val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
+ val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
val tacs = Rs |> map (fn R =>