# HG changeset patch
# User haftmann
# Date 1309553285 -7200
# Node ID 5967e25c74664072a409405241e0389d7c33d427
# Parent  e8ee3641754e7e1633ffd3e4c9f5c5ac3f791783# Parent  93cd6dd1a1c6472fb35be15ce09f223a7a2b4015
merged

diff -r e8ee3641754e -r 5967e25c7466 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Jul 01 19:42:07 2011 +0200
+++ b/src/Pure/Isar/code.ML	Fri Jul 01 22:48:05 2011 +0200
@@ -153,16 +153,19 @@
 
 (* datatypes *)
 
-datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list
+datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list *
+      string list (*references to associated case constructors*)
   | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
 
-fun constructors_of (Constructors cos) = (cos, false)
+fun constructors_of (Constructors (cos, _)) = (cos, false)
   | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
 
 
 (* functions *)
 
 datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy
+      (* (cache for default equations, lazy computation of default equations)
+         -- helps to restore natural order of default equations *)
   | Eqns of (thm * bool) list
   | Proj of term * string
   | Abstr of thm * string;
@@ -1160,16 +1163,26 @@
 
 fun add_case thm thy =
   let
-    val (case_const, (k, case_pats)) = case_cert thm;
-    val _ = case filter_out (is_constr thy) case_pats
+    val (case_const, (k, cos)) = case_cert thm;
+    val _ = case filter_out (is_constr thy) cos
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
-    val entry = (1 + Int.max (1, length case_pats), (k, case_pats));
+    val entry = (1 + Int.max (1, length cos), (k, cos));
+    fun register_case cong = (map_cases o apfst)
+      (Symtab.update (case_const, (entry, cong)));
+    fun register_for_constructors (Constructors (cos', cases)) =
+         Constructors (cos',
+           if exists (fn (co, _) => member (op =) cos co) cos'
+           then insert (op =) case_const cases
+           else cases)
+      | register_for_constructors (x as Abstractor _) = x;
+    val register_type = (map_typs o Symtab.map)
+      (K ((map o apsnd o apsnd) register_for_constructors));
   in
     thy
     |> Theory.checkpoint
     |> `(fn thy => case_cong thy case_const entry)
-    |-> (fn cong => (map_exec_purge o map_cases o apfst) (Symtab.update (case_const, (entry, cong))))
+    |-> (fn cong => map_exec_purge (register_case cong #> register_type))
   end;
 
 fun add_undefined c thy =
@@ -1182,7 +1195,7 @@
   let
     val (old_constrs, some_old_proj) =
       case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
-       of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
+       of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
         | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
         | [] => ([], NONE)
     val outdated_funs = case some_old_proj
@@ -1219,7 +1232,7 @@
   in
     thy
     |> fold (del_eqns o fst) constrs
-    |> register_type (tyco, (vs, Constructors cos))
+    |> register_type (tyco, (vs, Constructors (cos, [])))
     |> Datatype_Interpretation.data (tyco, serial ())
   end;