1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:22:37 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:48:06 2009 +0100
     1.3 @@ -693,7 +693,7 @@
     1.4  val _ =
     1.5    OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     1.6      (K.tag_proof K.prf_chain)
     1.7 -    (calc_args >> (Toplevel.proofs' o Calculation.finally_));
     1.8 +    (calc_args >> (Toplevel.proofs' o Calculation.finally));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "moreover" "augment calculation by current facts"