--- a/src/Tools/Code/code_thingol.ML Thu Apr 12 07:33:14 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Apr 12 10:29:45 2012 +0200
@@ -781,10 +781,14 @@
fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
- fun mk_constr c t = let val n = Code.args_number thy c
- in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
+ fun mk_constr NONE t = NONE
+ | mk_constr (SOME c) t = let val n = Code.args_number thy c
+ in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
+
val constrs = if null case_pats then []
else map2 mk_constr case_pats (nth_drop t_pos ts);
+ val constrs' = map_filter I constrs
+
fun casify naming constrs ty ts =
let
val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
@@ -817,12 +821,12 @@
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
- (constrs ~~ ts_clause);
+ (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause)));
in ((t, ty), clauses) end;
in
translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
- #>> rpair n) constrs
+ #>> rpair n) constrs'
##>> translate_typ thy algbr eqngr permissive ty
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
#-> (fn (((t, constrs), ty), ts) =>