# HG changeset patch
# User wenzelm
# Date 1437769222 -7200
# Node ID 2164e7b47454cd04da1f9c326dc1bfb4a4f35bd2
# Parent  4592a9118d0be9b0dbaab5220da6dc9e140c627e
proper context;

diff -r 4592a9118d0b -r 2164e7b47454 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jul 24 22:19:36 2015 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 24 22:20:22 2015 +0200
@@ -129,7 +129,7 @@
 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
 
 (*Forward reasoning using destruction rules.*)
-fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
+fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' assume_tac ctxt;
 
 (*Like forward_tac, but deletes the assumption after use.*)
 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);