# HG changeset patch
# User wenzelm
# Date 974410394 -3600
# Node ID 97247fd6f1f85488599035a68b9e76fd2b0ec877
# Parent  c21bee84cefecd16517bd06e25bd0116c26ab182
Proof.assert_forward;

diff -r c21bee84cefe -r 97247fd6f1f8 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Nov 16 19:03:26 2000 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Nov 16 22:33:14 2000 +0100
@@ -123,7 +123,7 @@
 
 fun calculate final opt_rules print state =
   let
-    val facts = Proof.the_facts state;
+    val facts = Proof.the_facts (Proof.assert_forward state);
 
     val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
@@ -157,7 +157,7 @@
 
 fun collect final print state =
   let
-    val facts = Proof.the_facts state;
+    val facts = Proof.the_facts (Proof.assert_forward state);
     val (initial, thms) =
       (case get_calculation state of
         None => (true, [])