merged

--- a/src/HOL/Map.thy	Fri Jan 23 15:37:12 2009 +0100
+++ b/src/HOL/Map.thy	Fri Jan 23 19:52:02 2009 +0100
@@ -503,6 +503,15 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+lemma dom_const [simp]:
+  "dom (\<lambda>x. Some y) = UNIV"
+  by auto
+
+lemma dom_if:
+  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
+  by (auto split: if_splits)
+
+
 (* Due to John Matthews - could be rephrased with dom *)
 lemma finite_map_freshness:
   "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>

--- a/src/HOL/Tools/datatype_case.ML	Fri Jan 23 15:37:12 2009 +0100
+++ b/src/HOL/Tools/datatype_case.ML	Fri Jan 23 19:52:02 2009 +0100
@@ -419,21 +419,21 @@
 
 (* destruct nested patterns *)
 
-fun strip_case' dest (pat, rhs) =
+fun strip_case'' dest (pat, rhs) =
   case dest (Term.add_free_names pat []) rhs of
     SOME (exp as Free _, clauses) =>
       if member op aconv (OldTerm.term_frees pat) exp andalso
         not (exists (fn (_, rhs') =>
           member op aconv (OldTerm.term_frees rhs') exp) clauses)
       then
-        maps (strip_case' dest) (map (fn (pat', rhs') =>
+        maps (strip_case'' dest) (map (fn (pat', rhs') =>
           (subst_free [(exp, pat')] pat, rhs')) clauses)
       else [(pat, rhs)]
   | _ => [(pat, rhs)];
 
 fun gen_strip_case dest t = case dest [] t of
     SOME (x, clauses) =>
-      SOME (x, maps (strip_case' dest) clauses)
+      SOME (x, maps (strip_case'' dest) clauses)
   | NONE => NONE;
 
 val strip_case = gen_strip_case oo dest_case;

--- a/src/Pure/Isar/class.ML	Fri Jan 23 15:37:12 2009 +0100
+++ b/src/Pure/Isar/class.ML	Fri Jan 23 19:52:02 2009 +0100
@@ -66,7 +66,7 @@
         val prop = thm |> Thm.prop_of |> Logic.unvarify
           |> Morphism.term (inst_morph $> eq_morph) 
           |> (map_types o map_atyps) (K aT);
-        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
+        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME is WRONG!*)
           THEN ALLGOALS (ProofContext.fact_tac [thm]);
       in Goal.prove_global thy [] [] prop (tac o #context) end;
     val assm_intro = Option.map prove_assm_intro