1.1 --- a/src/Pure/Isar/code.ML	Fri Jul 01 19:42:07 2011 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Jul 01 22:48:05 2011 +0200
     1.3 @@ -153,16 +153,19 @@
     1.4  
     1.5  (* datatypes *)
     1.6  
     1.7 -datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list
     1.8 +datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list *
     1.9 +      string list (*references to associated case constructors*)
    1.10    | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
    1.11  
    1.12 -fun constructors_of (Constructors cos) = (cos, false)
    1.13 +fun constructors_of (Constructors (cos, _)) = (cos, false)
    1.14    | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
    1.15  
    1.16  
    1.17  (* functions *)
    1.18  
    1.19  datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy
    1.20 +      (* (cache for default equations, lazy computation of default equations)
    1.21 +         -- helps to restore natural order of default equations *)
    1.22    | Eqns of (thm * bool) list
    1.23    | Proj of term * string
    1.24    | Abstr of thm * string;
    1.25 @@ -1160,16 +1163,26 @@
    1.26  
    1.27  fun add_case thm thy =
    1.28    let
    1.29 -    val (case_const, (k, case_pats)) = case_cert thm;
    1.30 -    val _ = case filter_out (is_constr thy) case_pats
    1.31 +    val (case_const, (k, cos)) = case_cert thm;
    1.32 +    val _ = case filter_out (is_constr thy) cos
    1.33       of [] => ()
    1.34        | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
    1.35 -    val entry = (1 + Int.max (1, length case_pats), (k, case_pats));
    1.36 +    val entry = (1 + Int.max (1, length cos), (k, cos));
    1.37 +    fun register_case cong = (map_cases o apfst)
    1.38 +      (Symtab.update (case_const, (entry, cong)));
    1.39 +    fun register_for_constructors (Constructors (cos', cases)) =
    1.40 +         Constructors (cos',
    1.41 +           if exists (fn (co, _) => member (op =) cos co) cos'
    1.42 +           then insert (op =) case_const cases
    1.43 +           else cases)
    1.44 +      | register_for_constructors (x as Abstractor _) = x;
    1.45 +    val register_type = (map_typs o Symtab.map)
    1.46 +      (K ((map o apsnd o apsnd) register_for_constructors));
    1.47    in
    1.48      thy
    1.49      |> Theory.checkpoint
    1.50      |> `(fn thy => case_cong thy case_const entry)
    1.51 -    |-> (fn cong => (map_exec_purge o map_cases o apfst) (Symtab.update (case_const, (entry, cong))))
    1.52 +    |-> (fn cong => map_exec_purge (register_case cong #> register_type))
    1.53    end;
    1.54  
    1.55  fun add_undefined c thy =
    1.56 @@ -1182,7 +1195,7 @@
    1.57    let
    1.58      val (old_constrs, some_old_proj) =
    1.59        case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
    1.60 -       of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
    1.61 +       of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
    1.62          | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
    1.63          | [] => ([], NONE)
    1.64      val outdated_funs = case some_old_proj
    1.65 @@ -1219,7 +1232,7 @@
    1.66    in
    1.67      thy
    1.68      |> fold (del_eqns o fst) constrs
    1.69 -    |> register_type (tyco, (vs, Constructors cos))
    1.70 +    |> register_type (tyco, (vs, Constructors (cos, [])))
    1.71      |> Datatype_Interpretation.data (tyco, serial ())
    1.72    end;
    1.73