# HG changeset patch
# User kleing
# Date 1081835251 -7200
# Node ID ea6e18e5c7a97d4fd07a5fc9d060ede73f9ed2b2
# Parent  e1a196985fc8b68d647499c18b3880e64591a1ae
fix moreover/this behaviour:
"this" after moreover/also is not = calculation, but remains unchanged.

diff -r e1a196985fc8 -r ea6e18e5c7a9 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Apr 13 07:45:07 2004 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Apr 13 07:47:31 2004 +0200
@@ -139,9 +139,13 @@
 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
   | maintain_calculation true calc state =
       state
       |> reset_calculation