--- a/Nominal/Parser.thy Thu Mar 18 12:32:03 2010 +0100
+++ b/Nominal/Parser.thy Thu Mar 18 14:05:49 2010 +0100
@@ -385,7 +385,8 @@
fun note_simp_suffix s th ctxt =
snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s),
[Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
- val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
+ val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"),
+ [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
val q_perm = map (lift_thm lthy14) raw_perm_def;