diff -r e8732350a29f -r d1d09177ec89 Nominal/Nominal2.thy
--- 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)