Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_syn.ML
changeset 30189 3633f560f4c3
parent 30173 eabece26b89b
child 30242 aea5d7fa7ef5 
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -693,7 +693,7 @@
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     (K.tag_proof K.prf_chain)
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"
isabelle