fixed typo
authorhaftmann
Sat, 31 Mar 2007 08:22:14 +0200
changeset 22555 d04a4c1b6ab2
parent 22554 d1499fff65d8
child 22556 b067fdca022d
fixed typo
src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 30 16:19:03 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Sat Mar 31 08:22:14 2007 +0200
@@ -422,7 +422,7 @@
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = 
+      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
     fun pr_def (MLFuns (funns as (funn :: funns'))) =
           let