author | haftmann |
Sat, 31 Mar 2007 08:22:14 +0200 | |
changeset 22555 | d04a4c1b6ab2 |
parent 22554 | d1499fff65d8 |
child 22556 | b067fdca022d |
--- 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