src/Pure/Isar/calculation.ML
changeset 6781 0db24da2a3c1
parent 6778 2f66eea8a025
child 6782 adf099e851ed
--- 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;