--- 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;