oops;
authorwenzelm
Fri Jun 04 20:10:07 1999 +0200 (1999-06-04)
changeset 67810db24da2a3c1
parent 6780 769cea1985e4
child 6782 adf099e851ed
oops;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Jun 04 19:58:06 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Jun 04 20:10:07 1999 +0200
     1.3 @@ -135,12 +135,13 @@
     1.4        (prt calc;
     1.5          state
     1.6          |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
     1.7 +        |> put_calculation calc
     1.8          |> have_thm calc
     1.9 -        |> (if final then I else Proof.reset_facts)))
    1.10 +        |> (if final then Proof.chain else Proof.reset_facts)))
    1.11    end;
    1.12  
    1.13 -val also = calculate false;
    1.14 -val finally = calculate true;
    1.15 +fun also prt = calculate false prt;
    1.16 +fun finally prt = calculate true prt;
    1.17  
    1.18  
    1.19