--- 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
--- 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;
--- 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 *)