# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268911923 -3600
# Node ID ef2809001664a5380d1e1291908526e10c426c1f
# Parent  be911e869fded335c11a11a96ce8fce5dd0a8005
Case_Names for _inducts. Does not work for _induct yet.

diff -r be911e869fde -r ef2809001664 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 18 12:09:59 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 12:32:03 2010 +0100
@@ -380,14 +380,15 @@
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
   val _ = tracing "Lifting induction";
-  val q_induct = lift_thm lthy13 induct;
+  val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
+  val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct);
   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 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; 
+  val q_perm = map (lift_thm lthy14) raw_perm_def;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;