src/Pure/Isar/isar_syn.ML
changeset 22573 2ac646ab2f6c
parent 22485 3a7d623485fa
child 22744 5cbe966d67a2
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 03 19:24:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 03 19:24:19 2007 +0200
     1.3 @@ -665,7 +665,7 @@
     1.4  val finallyP =
     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 moreoverP =
    1.11    OuterSyntax.command "moreover" "augment calculation by current facts"