1.1 --- a/src/Pure/Isar/code.ML	Thu Apr 12 07:33:14 2012 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Apr 12 10:29:45 2012 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    val is_constr: theory -> string -> bool
     1.5    val is_abstr: theory -> string -> bool
     1.6    val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
     1.7 -  val get_case_scheme: theory -> string -> (int * (int * string list)) option
     1.8 +  val get_case_scheme: theory -> string -> (int * (int * string option list)) option
     1.9    val get_case_cong: theory -> string -> thm option
    1.10    val undefineds: theory -> string list
    1.11    val print_codesetup: theory -> unit
    1.12 @@ -180,7 +180,7 @@
    1.13      (*with explicit history*),
    1.14    types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
    1.15      (*with explicit history*),
    1.16 -  cases: ((int * (int * string list)) * thm) Symtab.table * unit Symtab.table
    1.17 +  cases: ((int * (int * string option list)) * thm) Symtab.table * unit Symtab.table
    1.18  };
    1.19  
    1.20  fun make_spec (history_concluded, (functions, (types, cases))) =
    1.21 @@ -895,7 +895,7 @@
    1.22      fun analyze_cases cases =
    1.23        let
    1.24          val co_list = fold (AList.update (op =) o dest_case) cases [];
    1.25 -      in map (the o AList.lookup (op =) co_list) params end;
    1.26 +      in map (AList.lookup (op =) co_list) params end;
    1.27      fun analyze_let t =
    1.28        let
    1.29          val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
    1.30 @@ -948,10 +948,12 @@
    1.31                        :: Pretty.str "of"
    1.32                        :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
    1.33        );
    1.34 +    fun ignored_cases NONE = "<ignored>"
    1.35 +      | ignored_cases (SOME c) = string_of_const thy c
    1.36      fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
    1.37        | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
    1.38            Pretty.str (string_of_const thy const), Pretty.str "with",
    1.39 -          (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
    1.40 +          (Pretty.block o Pretty.commas o map (Pretty.str o ignored_cases)) cos];
    1.41      val functions = the_functions exec
    1.42        |> Symtab.dest
    1.43        |> (map o apsnd) (snd o fst)
    1.44 @@ -1087,7 +1089,7 @@
    1.45  fun add_case thm thy =
    1.46    let
    1.47      val (case_const, (k, cos)) = case_cert thm;
    1.48 -    val _ = case filter_out (is_constr thy) cos
    1.49 +    val _ = case map_filter I cos |> filter_out (is_constr thy)
    1.50       of [] => ()
    1.51        | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
    1.52      val entry = (1 + Int.max (1, length cos), (k, cos));
    1.53 @@ -1095,7 +1097,7 @@
    1.54        (Symtab.update (case_const, (entry, cong)));
    1.55      fun register_for_constructors (Constructors (cos', cases)) =
    1.56           Constructors (cos',
    1.57 -           if exists (fn (co, _) => member (op =) cos co) cos'
    1.58 +           if exists (fn (co, _) => member (op =) cos (SOME co)) cos'
    1.59             then insert (op =) case_const cases
    1.60             else cases)
    1.61        | register_for_constructors (x as Abstractor _) = x;
    1.62 @@ -1131,7 +1133,7 @@
    1.63              ((the_functions o the_exec) thy) [old_proj];
    1.64      fun drop_outdated_cases cases = fold Symtab.delete_safe
    1.65        (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
    1.66 -        if exists (member (op =) old_constrs) cos
    1.67 +        if exists (member (op =) old_constrs) (map_filter I cos)
    1.68            then insert (op =) c else I) cases []) cases;
    1.69    in
    1.70      thy

     2.1 --- a/src/Tools/Code/code_thingol.ML	Thu Apr 12 07:33:14 2012 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Apr 12 10:29:45 2012 +0200
     2.3 @@ -781,10 +781,14 @@
     2.4      fun arg_types num_args ty = fst (chop num_args (binder_types ty));
     2.5      val tys = arg_types num_args (snd c_ty);
     2.6      val ty = nth tys t_pos;
     2.7 -    fun mk_constr c t = let val n = Code.args_number thy c
     2.8 -      in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
     2.9 +    fun mk_constr NONE t = NONE
    2.10 +      | mk_constr (SOME c) t = let val n = Code.args_number thy c
    2.11 +        in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
    2.12 +
    2.13      val constrs = if null case_pats then []
    2.14        else map2 mk_constr case_pats (nth_drop t_pos ts);
    2.15 +    val constrs' = map_filter I constrs
    2.16 +
    2.17      fun casify naming constrs ty ts =
    2.18        let
    2.19          val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
    2.20 @@ -817,12 +821,12 @@
    2.21            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
    2.22            else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
    2.23              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
    2.24 -              (constrs ~~ ts_clause);
    2.25 +              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause)));
    2.26        in ((t, ty), clauses) end;
    2.27    in
    2.28      translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
    2.29      ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
    2.30 -      #>> rpair n) constrs
    2.31 +      #>> rpair n) constrs'
    2.32      ##>> translate_typ thy algbr eqngr permissive ty
    2.33      ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
    2.34      #-> (fn (((t, constrs), ty), ts) =>