# HG changeset patch
# User wenzelm
# Date 928519807 -7200
# Node ID 0db24da2a3c1a76c50854d366cfe07f9bc550053
# Parent  769cea1985e466142b674fa63097811e9d6883cc
oops;

diff -r 769cea1985e4 -r 0db24da2a3c1 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Jun 04 19:58:06 1999 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Jun 04 20:10:07 1999 +0200
@@ -135,12 +135,13 @@
       (prt calc;
         state
         |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
+        |> put_calculation calc
         |> have_thm calc
-        |> (if final then I else Proof.reset_facts)))
+        |> (if final then Proof.chain else Proof.reset_facts)))
   end;
 
-val also = calculate false;
-val finally = calculate true;
+fun also prt = calculate false prt;
+fun finally prt = calculate true prt;