# HG changeset patch
# User haftmann
# Date 1175322134 -7200
# Node ID d04a4c1b6ab21124f58862d8877ef36fa003a4fd
# Parent  d1499fff65d8794cbd4f5d57ee388a0a09cf7382
fixed typo

diff -r d1499fff65d8 -r d04a4c1b6ab2 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