diff -r 02a830bab542 -r a2c9506b62a7 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Dec 06 16:07:10 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Tue Dec 06 16:07:25 2005 +0100
@@ -595,7 +595,7 @@
 fun exprgen_sort_default thy defs sort trns =
   trns
   |> fold_map (ensure_def_class thy defs)
-       (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
+       (sort |> ClassPackage.syntactic_sort_of thy |> map (idf_of_name thy nsp_class))
   |-> (fn sort => succeed sort)
 
 fun exprgen_type_default thy defs (TVar _) trns =
@@ -763,17 +763,11 @@
 fun defgen_clsmem thy (defs as (_, _, _)) f trns =
   case name_of_idf thy nsp_mem f
    of SOME clsmem =>
-        let
-          val _ = debug 10 (fn _ => "CLSMEM " ^ quote clsmem) ();
-          val _ = debug 10 (fn _ => (the o ClassPackage.lookup_const_class thy) clsmem) ();
-          val cls = idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem);
-          val ty = ClassPackage.get_const_sign thy "'a" clsmem;
-        in
-          trns
-          |> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
-          |> (invoke_cg_type thy defs o devarify_type) ty
-          |-> (fn ty => succeed (Classmember (cls, "a", ty), []))
-        end
+        trns
+        |> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
+        |> ensure_def_class thy defs (idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem))
+        ||>> (invoke_cg_type thy defs o devarify_type) (ClassPackage.get_const_sign thy "'a" clsmem)
+        |-> (fn (cls, ty) => succeed (Classmember (cls, "a", ty), []))
     | _ =>
         trns |> fail ("no class member found for " ^ quote f)
 
@@ -1332,7 +1326,7 @@
     |> (if is_some consts then generate_code (the consts) else pair [])
     |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get)
           | consts => `(serializer' (SOME consts) o #modl o CodegenData.get))
-    |-> (fn code => (setmp print_mode [] (use_code o Pretty.output) code; I))
+    |-> (fn code => ((use_code o Pretty.output) code; I))
   end;