changeset 42495 | 1af81b70cf09 |
parent 42371 | 5900f06b4198 |
child 44113 | 0baa8bbd355a |
--- a/src/Pure/goal.ML Wed Apr 27 20:58:40 2011 +0200 +++ b/src/Pure/goal.ML Wed Apr 27 21:50:04 2011 +0200 @@ -326,7 +326,7 @@ fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => let - val ((_, goal'), ctxt') = Variable.focus goal ctxt; + val ((_, goal'), ctxt') = Variable.focus_cterm 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 =>