# HG changeset patch
# User wenzelm
# Date 1081880546 -7200
# Node ID 341908d6c792a17b6ee1b3e842058f9f106c6866
# Parent  b9cd48af3512e3b18f38478ab3b2411f7a3ab8fb
'also'/'moreover': do not interfere with current facts, allow in chain mode;

diff -r b9cd48af3512 -r 341908d6c792 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Apr 13 20:21:11 2004 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Apr 13 20:22:26 2004 +0200
@@ -134,18 +134,18 @@
 
 (** proof commands **)
 
+fun assert_sane final =
+  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
+
+
 (* maintain calculation register *)
 
 val calculationN = "calculation";
 
 fun maintain_calculation false calc state =
-    let val facts = Proof.the_facts state 
-    in
       state
       |> put_calculation calc
-      |> Proof.simple_have_thms calculationN calc
-      |> Proof.simple_have_thms Proof.thisN facts
-    end
+      |> Proof.put_thms (calculationN, calc)
   | maintain_calculation true calc state =
       state
       |> reset_calculation
@@ -172,7 +172,7 @@
       |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
       |> Seq.filter (not o projection ths);
 
-    val facts = Proof.the_facts (Proof.assert_forward state);
+    val facts = Proof.the_facts (assert_sane final state);
     val (initial, calculations) =
       (case get_calculation state of
         None => (true, Seq.single facts)
@@ -192,7 +192,7 @@
 
 fun collect final print state =
   let
-    val facts = Proof.the_facts (Proof.assert_forward state);
+    val facts = Proof.the_facts (assert_sane final state);
     val (initial, thms) =
       (case get_calculation state of
         None => (true, [])