# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268659925 -3600
# Node ID 378b8c791de8d5b863703e1931fb96dc02607f8e
# Parent  a93f8df272de1999d0507ff7dcaa4cb4792ab83f
derive "inducts" from "induct" instead of lifting again is much faster.

diff -r a93f8df272de -r 378b8c791de8 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 15 13:56:17 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 14:32:05 2010 +0100
@@ -398,8 +398,10 @@
   val q_name = space_implode "_" qty_names;
   val q_induct = lift_thm lthy13 induct;
   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 (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
+  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
diff -r a93f8df272de -r 378b8c791de8 Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 15 13:56:17 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 14:32:05 2010 +0100
@@ -24,11 +24,11 @@
 thm lam_bp_bn
 thm lam_bp_perm
 thm lam_bp_induct
+thm lam_bp_inducts
 thm lam_bp_distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 
 term "supp (x :: lam)"
-lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
 (* maybe should be added to Infinite.thy *)
 lemma infinite_Un:
@@ -306,6 +306,7 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
 
 (* example 3 from Peter Sewell's bestiary *)