--- a/Nominal/Ex/Height.thy	Fri Dec 31 12:12:59 2010 +0000
+++ b/Nominal/Ex/Height.thy	Fri Dec 31 13:31:39 2010 +0000
@@ -14,7 +14,6 @@
   | App "lam" "lam"
   | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100)
 
-thm lam.strong_induct
 
 text {* Definition of the height-function on lambda-terms. *} 
 
@@ -84,17 +83,17 @@
 theorem height_subst:
   shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
-  case (1 y)
+  case (Var y)
   have "1 \<le> height e'" by (rule height_ge_one)
   then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
 next
-  case (3 y e1)
+  case (Lam y e1)
   have ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by fact
   moreover
   have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *)
   ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
 next    
-  case (2 e1 e2)
+  case (App e1 e2)
   have ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" 
   and  ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by fact+
   then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp 

--- a/Nominal/Nominal2.thy	Fri Dec 31 12:12:59 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Dec 31 13:31:39 2010 +0000
@@ -131,12 +131,12 @@
   val dt_full_names' = add_raws dt_full_names
   val dts_env = dt_full_names ~~ dt_full_names'
 
-  val cnstrs = get_cnstr_strs dts
-  val cnstrs_ty = get_typed_cnstrs dts
-  val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
-  val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
-    (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
-  val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
+  val cnstr_names = get_cnstr_strs dts
+  val cnstr_tys = get_typed_cnstrs dts
+  val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names
+  val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
+    (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys
+  val cnstrs_env = cnstr_full_names ~~ cnstr_full_names'
 
   val bn_fun_strs = get_bn_fun_strs bn_funs
   val bn_fun_strs' = add_raws bn_fun_strs
@@ -153,7 +153,7 @@
 
   val lthy1 = Named_Target.theory_init thy1
 in
-  (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
+  (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1)
 end
 *}
 
@@ -174,7 +174,7 @@
 let
   (* definition of the raw datatypes *)
   val _ = warning "Definition of raw datatypes";
-  val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
+  val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) =
     if get_STEPS lthy > 0 
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
@@ -540,7 +540,7 @@
   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
-  val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
+  val qstrong_induct_thms =  prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
 
 
   (* noting the theorems *)  
@@ -549,6 +549,7 @@
   val thms_name = 
     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   fun thms_suffix s = Binding.qualified true s thms_name 
+  val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
@@ -559,11 +560,11 @@
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
-     ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
-     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
-     ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
-     ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
-     ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms)
+     ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts)
+     ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts)
+     ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms)
+     ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)