--- 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, [])