--- a/src/Pure/goal.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/goal.ML Mon Nov 10 21:49:48 2014 +0100
@@ -336,7 +336,7 @@
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 =>
- eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
+ eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt);
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
end;