src/Tools/Code/code_ml.ML
changeset 31874 f172346ba805
parent 31775 2b04504fcb69
child 31889 fb2c8a687529
--- a/src/Tools/Code/code_ml.ML	Tue Jun 30 14:53:59 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 14:54:00 2009 +0200
@@ -94,9 +94,9 @@
                [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) =
-              pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            fun pr (some_pat, ty) =
+              pr_bind is_closure thm NOBR (some_pat, ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,17 +122,15 @@
           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
     and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const thm vars
-    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), _) = concat [str v, str "as", p]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
@@ -146,7 +144,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
@@ -403,9 +401,8 @@
                 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
       | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -427,17 +424,15 @@
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
     and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const
-    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), _) = brackets [p, str "as", str v]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
@@ -449,7 +444,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
             brackets (