diff -r 2b2fbc32550e -r 6720b5010a57 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Dec 21 15:18:57 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Dec 21 15:19:16 2005 +0100
@@ -409,7 +409,6 @@
                 in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
     fun ml_from_funs (ds as d::ds_tl) =
       let
-        val _ = debug 15 (fn _ => "(1) FUN") ();
         fun mk_definer [] = "val"
           | mk_definer _ = "fun"
         fun check_args (_, Fun ((pats, _)::_, _)) NONE =
@@ -420,12 +419,9 @@
               else error ("mixing simultaneous vals and funs not implemented")
           | check_args _ _ =
               error ("function definition block containing other definitions than functions")
-        val _ = debug 15 (fn _ => "(2) FUN") ();
         val definer = the (fold check_args ds NONE);
-        val _ = debug 15 (fn _ => "(3) FUN") ();
         fun mk_eq definer f ty (pats, expr) =
           let
-            val _ = debug 15 (fn _ => "(5) FUN") ();
             fun mk_pat_arg p =
               case itype_of_ipat p
                of ty as IType (tyco, _) =>
@@ -439,20 +435,16 @@
                       ]
                     else ml_from_pat BR p
                 | _ => ml_from_pat BR p;
-            val _ = debug 15 (fn _ => "(6) FUN") ();
             val lhs = [Pretty.str (definer ^ " " ^ f)]
                        @ (if null pats
                           then [Pretty.str ":", ml_from_type NOBR ty]
                           else map mk_pat_arg pats)
-            val _ = debug 15 (fn _ => "(7) FUN") ();
             val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
-            val _ = debug 15 (fn _ => "(8) FUN") ();
           in
             Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
           end
         fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
           let
-            val _ = debug 15 (fn _ => "(4) FUN") ();
             val (pats_hd::pats_tl) = (fst o split_list) eqs;
             val shift = if null eq_tl then I else map (Pretty.block o single);
           in (Pretty.block o Pretty.fbreaks o shift) (
@@ -520,12 +512,11 @@
           NONE
       | ml_from_def (name, Classinst _) =
           error ("can't serialize instance declaration " ^ quote name ^ " to ML")
-  in (debug 10 (fn _ => "*** defs " ^ commas (map (fn (n, d) => n ^ " = " ^ (Pretty.output o pretty_def) d) ds)) ();
-  case ds
+  in case ds
    of (_, Fun _)::_ => ml_from_funs ds
     | (_, Datatypecons _)::_ => ml_from_datatypes ds
     | (_, Datatype _)::_ => ml_from_datatypes ds
-    | [d] => ml_from_def d)
+    | [d] => ml_from_def d
   end;
 
 in
@@ -561,7 +552,7 @@
         Pretty.str ("end; (* struct " ^ name ^ " *)")
       ]);
     fun is_dicttype tyco =
-      case get_def module tyco
+      NameSpace.is_qualified tyco andalso case get_def module tyco
        of Typesyn (_, IDictT _) => true
         | _ => false;
     fun eta_expander "Pair" = 2
@@ -588,7 +579,6 @@
           else 0;
   in
     module
-    |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "selecting submodule...")
     |> (if is_some select then (partof o the) select else I)
     |> debug 3 (fn _ => "eta-expanding...")
@@ -599,7 +589,6 @@
     |> tupelize_cons
     |> debug 3 (fn _ => "eliminating classes...")
     |> eliminate_classes
-    |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "serializing...")
     |> serialize (ml_from_defs tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root
     |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
@@ -894,9 +883,7 @@
           else error ("empty statement during serialization: " ^ quote name)
       | haskell_from_def (name, Fun (eqs, (_, ty))) =
           let
-            val _ = print "(1) FUN";
             fun from_eq name (args, rhs) =
-              (print args; print rhs;
               Pretty.block [
                 Pretty.str (lower_first name),
                 Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
@@ -904,8 +891,7 @@
                 Pretty.str ("="),
                 Pretty.brk 1,
                 haskell_from_expr NOBR rhs
-              ])
-            val _ = print "(2) FUN";
+              ]
           in
             Pretty.chunks [
               Pretty.block [
@@ -991,7 +977,7 @@
             ) instmems)
           ] |> SOME
   in
-    case List.mapPartial (fn (name, def) => (print ("serializing " ^ name); haskell_from_def (name, def))) defs
+    case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
      of [] => NONE
       | l => (SOME o Pretty.block) l
   end;
@@ -1047,7 +1033,6 @@
         | _ => false;
   in
     module
-    |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "selecting submodule...")
     |> (if is_some select then (partof o the) select else I)
     |> debug 3 (fn _ => "eta-expanding...")