merged

--- a/CONTRIBUTORS	Mon Oct 19 16:47:21 2009 +0200
+++ b/CONTRIBUTORS	Tue Oct 20 08:10:47 2009 +0200
@@ -7,6 +7,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* Oktober 2009: Florian Haftmann, TUM
+  Refinement of parts of the HOL datatype package
+
+* Oktober 2009: Florian Haftmann, TUM
+  Generic term styles for term antiquotations
+
 * September 2009: Thomas Sewell, NICTA
   More efficient HOL/record implementation
 
@@ -14,7 +20,7 @@
   SMT method using external SMT solvers
 
 * September 2009: Florian Haftmann, TUM
-  Refinement of Sets and Lattices
+  Refinement of sets and lattices
 
 * July 2009: Jeremy Avigad and Amine Chaieb
   New number theory

--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 08:10:47 2009 +0200
@@ -7,8 +7,6 @@
 signature DATATYPE_CODEGEN =
 sig
   val find_shortest_path: Datatype.descr -> int -> (string * int) option
-  val mk_eq_eqns: theory -> string -> (thm * bool) list
-  val mk_case_cert: theory -> string -> thm
   val setup: theory -> theory
 end;
 
@@ -386,7 +384,7 @@
       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
-  in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
+  in (map prove (triv_injects @ injects @ distincts), prove refl) end;
 
 fun add_equality vs dtcos thy =
   let
@@ -405,14 +403,12 @@
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
       THEN ALLGOALS (ProofContext.fact_tac thms);
-    fun add_eq_thms dtco thy =
-      let
-        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
-        val thy_ref = Theory.check_thy thy;
-        fun mk_thms () = rev ((mk_eq_eqns (Theory.deref thy_ref) dtco));
-      in
-        Code.add_eqnl (const, Lazy.lazy mk_thms) thy
-      end;
+    fun add_eq_thms dtco =
+      Theory.checkpoint
+      #> `(fn thy => mk_eq_eqns thy dtco)
+      #-> (fn (thms, thm) =>
+        Code.add_nbe_eqn thm
+        #> fold_rev Code.add_eqn thms);
   in
     thy
     |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])

--- a/src/Pure/Isar/code.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 20 08:10:47 2009 +0200
@@ -37,7 +37,6 @@
     (string * ((string * sort) list * (string * typ list) list)
       -> theory -> theory) -> theory -> theory
   val add_eqn: thm -> theory -> theory
-  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
@@ -119,19 +118,8 @@
 
 (* code equations *)
 
-type eqns = bool * (thm * bool) list lazy;
-  (*default flag, theorems with proper flag (perhaps lazy)*)
-
-fun pretty_lthms ctxt r = case Lazy.peek r
- of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms)
-  | NONE => [Pretty.str "[...]"];
-
-fun certificate thy f r =
-  case Lazy.peek r
-   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
-    | NONE => let
-        val thy_ref = Theory.check_thy thy;
-      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
+type eqns = bool * (thm * bool) list;
+  (*default flag, theorems with proper flag *)
 
 fun add_drop_redundant thy (thm, proper) thms =
   let
@@ -148,13 +136,11 @@
       else false;
   in (thm, proper) :: filter_out drop thms end;
 
-fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
-  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
-  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
+fun add_thm thy _ thm (false, thms) = (false, add_drop_redundant thy thm thms)
+  | add_thm thy true thm (true, thms) = (true, thms @ [thm])
+  | add_thm thy false thm (true, thms) = (false, [thm]);
 
-fun add_lthms lthms _ = (false, lthms);
-
-fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
+fun del_thm thm = apsnd (remove (eq_fst Thm.eq_thm_prop) (thm, true));
 
 
 (* executable code data *)
@@ -285,17 +271,17 @@
 val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
 
 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
-  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
+  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
     o apfst) (fn (_, eqns) => (true, f eqns));
 
-fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
+fun del_eqns c = change_eqns true c (K (false, []));
 
 
 (* tackling equation history *)
 
 fun get_eqns thy c =
   Symtab.lookup ((the_eqns o the_exec) thy) c
-  |> Option.map (Lazy.force o snd o snd o fst)
+  |> Option.map (snd o snd o fst)
   |> these;
 
 fun continue_history thy = if (history_concluded o the_exec) thy
@@ -550,7 +536,7 @@
 
 fun all_eqns thy =
   Symtab.dest ((the_eqns o the_exec) thy)
-  |> maps (Lazy.force o snd o snd o fst o snd);
+  |> maps (snd o snd o fst o snd);
 
 
 (* cases *)
@@ -606,9 +592,9 @@
   let
     val ctxt = ProofContext.init thy;
     val exec = the_exec thy;
-    fun pretty_eqn (s, (_, lthms)) =
+    fun pretty_eqns (s, (_, eqns)) =
       (Pretty.block o Pretty.fbreaks) (
-        Pretty.str s :: pretty_lthms ctxt lthms
+        Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns
       );
     fun pretty_dtyp (s, []) =
           Pretty.str s
@@ -638,7 +624,7 @@
       Pretty.block (
         Pretty.str "code equations:"
         :: Pretty.fbrk
-        :: (Pretty.fbreaks o map pretty_eqn) eqns
+        :: (Pretty.fbreaks o map pretty_eqns) eqns
       ),
       Pretty.block (
         Pretty.str "datatypes:"
@@ -704,11 +690,6 @@
 fun add_nbe_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, false)) thy;
 
-fun add_eqnl (c, lthms) thy =
-  let
-    val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
-  in change_eqns false c (add_lthms lthms') thy end;
-
 val add_default_eqn_attribute = Thm.declaration_attribute
   (fn thm => Context.mapping (add_default_eqn thm) I);
 val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);