# HG changeset patch
# User haftmann
# Date 1166705715 -3600
# Node ID 6cbc0f69a21c1b4223bdebdcd25f05382dd13bdc
# Parent  1a0e32ccb8bb8d19a4c432a89a8376aa5a34eebf
clarified code

diff -r 1a0e32ccb8bb -r 6cbc0f69a21c src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Thu Dec 21 13:55:14 2006 +0100
+++ b/src/Pure/Tools/codegen_consts.ML	Thu Dec 21 13:55:15 2006 +0100
@@ -106,29 +106,16 @@
     val inst_signs = (map o apsnd o map_type_tfree) (K ty_inst) cs;
   in (sort_args, inst_signs) end;
 
-fun disc_typ_of_classop thy (c, [TVar _]) = 
-      let
-        val class = (the o AxClass.class_of_param thy) c;
-        val (v, cs) = AxClass.params_of_class thy class;
-      in
-        (Logic.varifyT o map_type_tfree (K (TFree (v, [class]))))
-          ((the o AList.lookup (op =) cs) c)
-      end
-  | disc_typ_of_classop thy (c, [TFree _]) = 
-      let
-        val class = (the o AxClass.class_of_param thy) c;
-        val (v, cs) = AxClass.params_of_class thy class;
-      in
-        (Logic.varifyT o map_type_tfree (K (TFree (v, [class]))))
-          ((the o AList.lookup (op =) cs) c)
-      end
-  | disc_typ_of_classop thy (c, [Type (tyco, _)]) =
-      let
-        val class = (the o AxClass.class_of_param thy) c;
-        val (_, cs) = instance_dict thy (class, tyco);
-      in
-        Logic.varifyT ((the o AList.lookup (op =) cs) c)
-      end;
+fun disc_typ_of_classop thy (c, [ty]) = 
+  let
+    val class = (the o AxClass.class_of_param thy) c;
+    val cs = case ty
+     of TVar _ => snd (AxClass.params_of_class thy class)
+      | TFree _ => snd (AxClass.params_of_class thy class)
+      | Type (tyco, _) => snd (instance_dict thy (class, tyco));
+  in
+    (Logic.varifyT o the o AList.lookup (op =) cs) c
+  end;
 
 fun disc_typ_of_const thy f (const as (c, [ty])) =
       if (is_some o AxClass.class_of_param thy) c
diff -r 1a0e32ccb8bb -r 6cbc0f69a21c src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Thu Dec 21 13:55:14 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Thu Dec 21 13:55:15 2006 +0100
@@ -101,7 +101,7 @@
 
 fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
   let
-    val (v, cs) = (AxClass.params_of_class thy) class;
+    val (v, cs) = AxClass.params_of_class thy class;
     val superclasses = (proj_sort o Sign.super_classes thy) class;
     val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
     val class' = CodegenNames.class thy class;
diff -r 1a0e32ccb8bb -r 6cbc0f69a21c src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:14 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:15 2006 +0100
@@ -150,9 +150,9 @@
   end;
 
 fun parse_args f args =
-  case f args
-   of (x, []) => x
-    | (_, _) => error "bad serializer arguments";
+  case Scan.read Args.stopper f args
+   of SOME x => x
+    | NONE => error "bad serializer arguments";
 
 
 (* list and string serializer *)