--- a/Nominal/LFex.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
-  apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
   apply(simp_all only: eqvts[symmetric])
   apply(simp_all only: Collect_neg_conj)
@@ -57,7 +57,7 @@
 
 lemma supp_fv:
   "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
-  apply(induct rule: kind_ty_trm_induct)
+  apply(induct rule: kind_ty_trm.induct)
   apply(simp_all (no_asm) only: supp_eqs)
   apply(simp_all)
   apply(simp_all add: supp_eqs)

--- a/Nominal/Parser.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -379,16 +379,16 @@
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
+  fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = tracing "Lifting induction";
   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"),
+    snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
+  val (_, lthy14) = Local_Theory.note ((suffix_bind "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 (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   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;
@@ -401,7 +401,7 @@
   val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17;
+  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;

--- a/Nominal/Test.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -22,22 +22,22 @@
 
 lemma finite_fv:
   shows "finite (fv_lm t)"
-apply(induct t rule: lm_induct)
+apply(induct t rule: lm.induct)
 apply(simp_all)
 done
 
 lemma supp_fn:
   shows "supp t = fv_lm t"
-apply(induct t rule: lm_induct)
+apply(induct t rule: lm.induct)
 apply(simp_all)
 apply(simp only: supp_def)
-apply(simp only: lm_perm)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.perm)
+apply(simp only: lm.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lm_perm)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.perm)
+apply(simp only: lm.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -45,9 +45,9 @@
 apply(simp only: supp_def[symmetric])
 apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -56,7 +56,7 @@
 apply(simp only: supp_Abs)
 done
 
-lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]]
+lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]]
 
 lemma
   fixes c::"'a::fs"
@@ -66,10 +66,10 @@
   shows "P c lm"
 proof -
   have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm_induct)
-    apply(simp only: lm_perm)
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
     apply(rule a1)
-    apply(simp only: lm_perm)
+    apply(simp only: lm.perm)
     apply(rule a2)
     apply(blast)[1]
     apply(assumption)
@@ -77,9 +77,9 @@
     apply(erule exE)
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp del: lm_perm)
-    apply(subst lm_perm)
-    apply(subst (2) lm_perm)
+    apply(simp del: lm.perm)
+    apply(subst lm.perm)
+    apply(subst (2) lm.perm)
     apply(rule flip_fresh_fresh)
     apply(simp add: fresh_def)
     apply(simp only: supp_fn')
@@ -111,13 +111,13 @@
 where
   "bi (BP x t) = {atom x}"
 
-thm lam_bp_fv
-thm lam_bp_eq_iff
-thm lam_bp_bn
-thm lam_bp_perm
-thm lam_bp_induct
-thm lam_bp_inducts
-thm lam_bp_distinct
+thm lam_bp.fv
+thm lam_bp.eq_iff
+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)"
@@ -129,18 +129,18 @@
 lemma supp_fv:
   shows "supp t = fv_lam t" 
   and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
-apply(induct t and bp rule: lam_bp_inducts)
+apply(induct t and bp rule: lam_bp.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.perm)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.perm)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -148,9 +148,9 @@
 (* LAM case *)
 apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -160,9 +160,9 @@
 (* LET case *)
 apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
@@ -178,8 +178,8 @@
 apply(blast)
 (* BP case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.perm)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -189,7 +189,7 @@
 apply(simp)
 done
 
-thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
 ML {* val _ = recursive := true *}
 
@@ -205,30 +205,30 @@
 where
   "bi' (BP' x t) = {atom x}"
 
-thm lam'_bp'_fv
-thm lam'_bp'_eq_iff[no_vars]
-thm lam'_bp'_bn
-thm lam'_bp'_perm
-thm lam'_bp'_induct
-thm lam'_bp'_inducts
-thm lam'_bp'_distinct
+thm lam'_bp'.fv
+thm lam'_bp'.eq_iff[no_vars]
+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}) *}
 
 lemma supp_fv':
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
-apply(induct t and bp rule: lam'_bp'_inducts)
+apply(induct t and bp rule: lam'_bp'.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.perm)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.perm)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -236,9 +236,9 @@
 (* LAM case *)
 apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -249,9 +249,9 @@
 apply(rule_tac t="supp (LET' bp' lam')" and 
                s="supp (Abs (bi' bp') (bp', lam'))" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen)
 apply(simp only: eqvts split_def fst_conv snd_conv)
@@ -260,8 +260,8 @@
 apply(simp add: supp_Abs supp_Pair)
 apply blast
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.perm)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -271,7 +271,7 @@
 apply simp
 done
 
-thm lam'_bp'_fv[simplified supp_fv'[symmetric]]
+thm lam'_bp'.fv[simplified supp_fv'[symmetric]]
 
 
 text {* example 2 *}
@@ -293,28 +293,28 @@
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
 
-thm trm'_pat'_fv
-thm trm'_pat'_eq_iff
-thm trm'_pat'_bn
-thm trm'_pat'_perm
-thm trm'_pat'_induct
-thm trm'_pat'_distinct
+thm trm'_pat'.fv
+thm trm'_pat'.eq_iff
+thm trm'_pat'.bn
+thm trm'_pat'.perm
+thm trm'_pat'.induct
+thm trm'_pat'.distinct
 
 lemma supp_fv_trm'_pat':
   shows "supp t = fv_trm' t" 
   and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
-apply(induct t and bp rule: trm'_pat'_inducts)
+apply(induct t and bp rule: trm'_pat'.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.perm)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.perm)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -322,9 +322,9 @@
 (* LAM case *)
 apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -335,9 +335,9 @@
 apply(rule_tac t="supp (Let pat' trm'1 trm'2)" 
            and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
@@ -353,20 +353,20 @@
 apply(blast)
 (* PN case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.perm)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp)
 (* PS case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.perm)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp)
 (* PD case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.perm)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -375,7 +375,7 @@
 apply(simp add: supp_at_base)
 done
 
-thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
+thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -393,12 +393,12 @@
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
-thm trm0_pat0_fv
-thm trm0_pat0_eq_iff
-thm trm0_pat0_bn
-thm trm0_pat0_perm
-thm trm0_pat0_induct
-thm trm0_pat0_distinct
+thm trm0_pat0.fv
+thm trm0_pat0.eq_iff
+thm trm0_pat0.bn
+thm trm0_pat0.perm
+thm trm0_pat0.induct
+thm trm0_pat0.distinct
 
 text {* example type schemes *}
 
@@ -408,12 +408,12 @@
 and  tyS =
   All xs::"name set" ty::"t" bind xs in ty
 
-thm t_tyS_fv
-thm t_tyS_eq_iff
-thm t_tyS_bn
-thm t_tyS_perm
-thm t_tyS_induct
-thm t_tyS_distinct
+thm t_tyS.fv
+thm t_tyS.eq_iff
+thm t_tyS.bn
+thm t_tyS.perm
+thm t_tyS.induct
+thm t_tyS.distinct
 
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
@@ -431,25 +431,25 @@
   and   S::"tyS"
   shows "finite (fv_t T)" 
   and   "finite (fv_tyS S)"
-apply(induct T and S rule: t_tyS_inducts)
-apply(simp_all add: t_tyS_fv)
+apply(induct T and S rule: t_tyS.inducts)
+apply(simp_all add: t_tyS.fv)
 done
 
 lemma supp_fv_t_tyS:
   shows "supp T = fv_t T" 
   and   "supp S = fv_tyS S"
-apply(induct T and S rule: t_tyS_inducts)
+apply(induct T and S rule: t_tyS.inducts)
 apply(simp_all)
 (* VarTS case *)
 apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.perm)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* FunTS case *)
 apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.perm)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -457,9 +457,9 @@
 (* All case *)
 apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS.perm)
 apply(simp only: permute_ABS)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
 apply(simp only: alpha_gen)
@@ -489,12 +489,12 @@
 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
 
-thm trm1_bp1_fv
-thm trm1_bp1_eq_iff
-thm trm1_bp1_bn
-thm trm1_bp1_perm
-thm trm1_bp1_induct
-thm trm1_bp1_distinct
+thm trm1_bp1.fv
+thm trm1_bp1.eq_iff
+thm trm1_bp1.bn
+thm trm1_bp1.perm
+thm trm1_bp1.induct
+thm trm1_bp1.distinct
 
 text {* example 3 from Terms.thy *}
 
@@ -512,12 +512,12 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
-thm trm3_rassigns3_fv
-thm trm3_rassigns3_eq_iff
-thm trm3_rassigns3_bn
-thm trm3_rassigns3_perm
-thm trm3_rassigns3_induct
-thm trm3_rassigns3_distinct
+thm trm3_rassigns3.fv
+thm trm3_rassigns3.eq_iff
+thm trm3_rassigns3.bn
+thm trm3_rassigns3.perm
+thm trm3_rassigns3.induct
+thm trm3_rassigns3.distinct
 
 (* example 5 from Terms.thy *)
 
@@ -534,12 +534,12 @@
   "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
-thm trm5_lts_fv
-thm trm5_lts_eq_iff
-thm trm5_lts_bn
-thm trm5_lts_perm
-thm trm5_lts_induct
-thm trm5_lts_distinct
+thm trm5_lts.fv
+thm trm5_lts.eq_iff
+thm trm5_lts.bn
+thm trm5_lts.perm
+thm trm5_lts.induct
+thm trm5_lts.distinct
 
 (* example from my PHD *)
 
@@ -554,12 +554,12 @@
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
 
-thm phd_fv
-thm phd_eq_iff
-thm phd_bn
-thm phd_perm
-thm phd_induct
-thm phd_distinct
+thm phd.fv
+thm phd.eq_iff
+thm phd.bn
+thm phd.perm
+thm phd.induct
+thm phd.distinct
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -614,13 +614,13 @@
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_eq_iff
-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
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
+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 *)
 
@@ -640,12 +640,12 @@
 | "bp'' (PUnit) = {}"
 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 
-thm exp_pat3_fv
-thm exp_pat3_eq_iff
-thm exp_pat3_bn
-thm exp_pat3_perm
-thm exp_pat3_induct
-thm exp_pat3_distinct
+thm exp_pat3.fv
+thm exp_pat3.eq_iff
+thm exp_pat3.bn
+thm exp_pat3.perm
+thm exp_pat3.induct
+thm exp_pat3.distinct
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -663,12 +663,12 @@
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
-thm exp6_pat6_fv
-thm exp6_pat6_eq_iff
-thm exp6_pat6_bn
-thm exp6_pat6_perm
-thm exp6_pat6_induct
-thm exp6_pat6_distinct
+thm exp6_pat6.fv
+thm exp6_pat6.eq_iff
+thm exp6_pat6.bn
+thm exp6_pat6.perm
+thm exp6_pat6.induct
+thm exp6_pat6.distinct
 
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 

--- a/Nominal/TySch.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -16,16 +16,16 @@
 and tyS =
   All xs::"name set" ty::"t" bind xs in ty
 
-thm t_tyS_fv
-thm t_tyS_eq_iff
-thm t_tyS_bn
-thm t_tyS_perm
-thm t_tyS_induct
-thm t_tyS_distinct
+thm t_tyS.fv
+thm t_tyS.eq_iff
+thm t_tyS.bn
+thm t_tyS.perm
+thm t_tyS.induct
+thm t_tyS.distinct
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
   apply(auto)
@@ -34,7 +34,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alpha_gen fresh_star_def eqvts)
   apply auto
@@ -42,18 +42,18 @@
 
 lemma
   shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
 oops
 
 lemma
   assumes a: "a \<noteq> b"
   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
   using a
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
   apply auto
   done