1.1 --- a/src/Pure/Isar/code.ML	Fri Jul 01 23:10:27 2011 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Jul 01 23:31:23 2011 +0200
     1.3 @@ -160,6 +160,8 @@
     1.4  fun constructors_of (Constructors (cos, _)) = (cos, false)
     1.5    | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
     1.6  
     1.7 +fun case_consts_of (Constructors (_, case_consts)) = case_consts
     1.8 +  | case_consts_of (Abstractor _) = [];
     1.9  
    1.10  (* functions *)
    1.11  
    1.12 @@ -213,12 +215,15 @@
    1.13          val history = if null filtered_history
    1.14            then raw_history else filtered_history;
    1.15        in ((false, (snd o hd) history), history) end;
    1.16 -    val all_constructors =
    1.17 -      maps (map fst o fst o constructors_of o snd o snd o hd o snd) (Symtab.dest types);
    1.18 +    val all_datatype_specs = map (snd o snd o hd o snd) (Symtab.dest types);
    1.19 +    val all_constructors = maps (map fst o fst o constructors_of) all_datatype_specs;
    1.20 +    val all_case_consts = maps (case_consts_of) all_datatype_specs;
    1.21      val functions = Symtab.join (K merge_functions) (functions1, functions2)
    1.22        |> fold (fn c => Symtab.map_entry c (apfst (K (true, empty_fun_spec)))) all_constructors;
    1.23 -    val cases = (Symtab.merge (K true) (cases1, cases2),
    1.24 -      Symtab.merge (K true) (undefs1, undefs2));
    1.25 +    val proto_cases = Symtab.merge (K true) (cases1, cases2);
    1.26 +    val illegal_cases = subtract (op =) all_case_consts (Symtab.keys proto_cases);
    1.27 +    val cases = (Symtab.merge (K true) (cases1, cases2)
    1.28 +      |> fold Symtab.delete illegal_cases, Symtab.merge (K true) (undefs1, undefs2));
    1.29    in make_spec (false, ((signatures, functions), (types, cases))) end;
    1.30  
    1.31  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;