src/Pure/Isar/calculation.ML
changeset 10478 97247fd6f1f8
parent 10008 61eb9f3aa92a
child 11097 c1be9f2dff4c
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Nov 16 19:03:26 2000 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Nov 16 22:33:14 2000 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5  fun calculate final opt_rules print state =
     1.6    let
     1.7 -    val facts = Proof.the_facts state;
     1.8 +    val facts = Proof.the_facts (Proof.assert_forward state);
     1.9  
    1.10      val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
    1.11      val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
    1.12 @@ -157,7 +157,7 @@
    1.13  
    1.14  fun collect final print state =
    1.15    let
    1.16 -    val facts = Proof.the_facts state;
    1.17 +    val facts = Proof.the_facts (Proof.assert_forward state);
    1.18      val (initial, thms) =
    1.19        (case get_calculation state of
    1.20          None => (true, [])