--- a/Nominal/Fv.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -174,7 +174,7 @@
       in
         if arg_no mem args_in_bn then 
           (if is_rec_type dt then
-            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good")
+            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
           else @{term "{} :: atom set"}) else
         if is_atom thy ty then mk_single_atom x else
         if is_atom_set thy ty then mk_atoms x else
@@ -384,7 +384,7 @@
   val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
-  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)
+(*  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   val (fvs2, lthy'') =
@@ -696,4 +696,14 @@
       | SOME i => i
 *}
 
+ML {*
+fun rename_vars fnctn thm =
+let
+  val vars = Term.add_vars (prop_of thm) []
+  val nvars = map (Var o ((apfst o apfst) fnctn)) vars
+in
+  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
 end
+*}
+
+end

--- a/Nominal/Parser.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -253,7 +253,13 @@
 end
 *}
 
-ML {* add_primrec_wrapper *}
+ML {*
+fun un_raw name = unprefix "_raw" name handle Fail _ => name
+fun add_under names = hd names :: (map (prefix "_") (tl names))
+fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
+val un_raw_names = rename_vars un_raws
+fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+*}
 
 lemma equivp_hack: "equivp x"
 sorry
@@ -269,8 +275,13 @@
 end
 *}
 
-ML {* val restricted_nominal=ref 0 *}
-ML {* val cheat_alpha_eqvt = ref true *}
+(* These 2 are critical, we don't know how to do it in term5 *)
+ML {* val cheat_fv_rsp = ref true *}
+ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+
+(* Fixes for these 2 are known *)
+ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -302,9 +313,13 @@
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
   val alpha_ts_loc = #preds alpha
+  val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
+  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
+  val fv_ts_nobn = List.take (fv_ts, length perms)
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
@@ -321,27 +336,24 @@
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
-else
-let
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
-    ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
+  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+  val fv_eqvt_tac =
+    if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
+    else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
-  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
+  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
+(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
+    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
   val lthy7 = define_quotient_type
-    (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts))
+    (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
@@ -351,56 +363,55 @@
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
-in
-if !restricted_nominal = 1 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
-else
-let
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
-  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts
-    (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9;
-  val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10
-  val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11;
-  val qfv_names = map (fn x => "fv_" ^ x) qty_names
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def 1;
+  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
+  val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
+    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
+    else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1
+  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
   val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
-  val thy = Local_Theory.exit_global lthy12b;
+  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+  val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   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;
-  val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
+  val q_induct = lift_thm lthy13 induct;
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
-  val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def;
+  val q_perm = map (lift_thm lthy14) raw_perm_def;
   val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
-  val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def;
+  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 (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
+  val q_bn = map (lift_thm lthy16) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
   val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
-  val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
+  val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
   val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
-  val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+  val q_dis = map (lift_thm lthy18) rel_dists;
   val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
-  val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt;
+  val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 in
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
-end
-end
 *}
 
+
 ML {* 
 (* parsing the datatypes and declaring *)
 (* constructors in the local theory    *)

--- a/Nominal/Rsp.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -87,13 +87,18 @@
 *}
 
 ML {*
+  fun all_eqvts ctxt =
+    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+ML {*
 fun constr_rsp_tac inj rsp equivps =
 let
   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
 in
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    rtac @{thm exI[of _ "0 :: perm"]} THEN'
    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
@@ -120,20 +125,28 @@
 *)
 
 ML {*
-fun build_eqvts bind funs perms simps induct ctxt =
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+
+ML {*
+fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
+*}
+
+ML {*
+fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
-  fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
-  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
+  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
+  fun eqvtc (fnctn, arg) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
+  val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames)
   val thms = HOLogic.conj_elims thm
 in
   Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
@@ -145,14 +158,6 @@
 apply (rule_tac x="pi \<bullet> pia" in exI)
 by auto
 
-ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-ML {*
-  fun all_eqvts ctxt =
-    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
 
 ML {*
 fun mk_minimal_ss ctxt =
@@ -195,8 +200,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt perms simps inducts (t, n) =
-  build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n)
+fun build_bv_eqvt simps inducts (t, n) ctxt =
+  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
 *}
 
 end

--- a/Nominal/Term5.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Term5.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -48,25 +48,32 @@
   done
 
 lemma alpha5_eqvt:
-  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
-  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)"
-apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-apply (simp_all add: alpha5_inj permute_eqvt[symmetric])
-apply (erule exE)
-apply (rule_tac x="x \<bullet> pi" in exI)
-apply (erule conjE)+
-apply (rule conjI)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: eqvts)
-apply (simp add: permute_eqvt[symmetric])
-apply (subst eqvts[symmetric])
-apply (simp add: eqvts)
+  "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
+  (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
+  (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
 done
 
+lemma alpha5_reflp:
+"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
+apply (rule rtrm5_rlts.induct)
+apply (simp_all add: alpha5_inj)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
+done
+
+lemma alpha5_symp:
+"(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (simp_all add: alpha5_inj)
+sorry
+
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
   "equivp alpha_rlts"
+  "equivp (alpha_rbv5 p)"
   sorry
 
 quotient_type

--- a/Nominal/Test.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -15,21 +15,18 @@
 where
   "bi (BP x t) = {atom x}"
 
+thm lam_bp_fv
+thm lam_bp_inject
+thm lam_bp_bn
+thm lam_bp_perm
+thm lam_bp_induct
+thm lam_bp_distinct
+
 (* compat should be
 compat (BP x t) pi (BP x' t')
   \<equiv> alpha_trm t t' \<and> pi o x = x'
 *)
 
-typ lam_raw
-term VAR_raw
-term APP_raw
-term LET_raw
-term Test.BP_raw
-thm bi_raw.simps
-thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
-thm fv_lam_raw_fv_bp_raw.simps[no_vars]
-
 text {* example 2 *}
 
 nominal_datatype trm' =
@@ -48,6 +45,12 @@
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
 
+thm trm'_pat'_fv
+thm trm'_pat'_inject
+thm trm'_pat'_bn
+thm trm'_pat'_perm
+thm trm'_pat'_induct
+thm trm'_pat'_distinct
 
 (* compat should be
 compat (PN) pi (PN) == True
@@ -55,16 +58,6 @@
 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
 *)
 
-
-thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
-thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
-thm f_raw.simps
-(*thm trm'_pat'_induct
-thm trm'_pat'_perm
-thm trm'_pat'_fv
-thm trm'_pat'_bn
-thm trm'_pat'_inject*)
-
 nominal_datatype trm0 =
   Var0 "name"
 | App0 "trm0" "trm0"
@@ -81,20 +74,28 @@
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
-thm f0_raw.simps
-(*thm trm0_pat0_induct
+thm trm0_pat0_fv
+thm trm0_pat0_inject
+thm trm0_pat0_bn
 thm trm0_pat0_perm
-thm trm0_pat0_fv
-thm trm0_pat0_bn*)
+thm trm0_pat0_induct
+thm trm0_pat0_distinct
 
 text {* example type schemes *}
 
 nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
+  VarTS "name"
+| FunTS "t" "t"
 and  tyS =
   All xs::"name set" ty::"t" bind xs in ty
 
+thm t_tyS_fv
+thm t_tyS_inject
+thm t_tyS_bn
+thm t_tyS_perm
+thm t_tyS_induct
+thm t_tyS_distinct
+
 (* example 1 from Terms.thy *)
 
 nominal_datatype trm1 =
@@ -113,8 +114,12 @@
 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
 
-
-thm bv1_raw.simps
+thm trm1_bp1_fv
+thm trm1_bp1_inject
+thm trm1_bp1_bn
+thm trm1_bp1_perm
+thm trm1_bp1_induct
+thm trm1_bp1_distinct
 
 text {* example 3 from Terms.thy *}
 
@@ -132,6 +137,12 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
+thm trm3_rassigns3_fv
+thm trm3_rassigns3_inject
+thm trm3_rassigns3_bn
+thm trm3_rassigns3_perm
+thm trm3_rassigns3_induct
+thm trm3_rassigns3_distinct
 
 (* compat should be
 compat (ANil) pi (PNil) \<equiv> TRue
@@ -153,6 +164,13 @@
   "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
+thm trm5_lts_fv
+thm trm5_lts_inject
+thm trm5_lts_bn
+thm trm5_lts_perm
+thm trm5_lts_induct
+thm trm5_lts_distinct
+
 (* example from my PHD *)
 
 atom_decl coname
@@ -166,9 +184,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 alpha_phd_raw.intros[no_vars]
-thm fv_phd_raw.simps[no_vars]
-
+thm phd_fv
+thm phd_inject
+thm phd_bn
+thm phd_perm
+thm phd_induct
+thm phd_distinct
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -223,8 +244,15 @@
 | "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_inject
+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_distinct
 
 (* example 3 from Peter Sewell's bestiary *)
+
 nominal_datatype exp =
   VarP "name"
 | AppP "exp" "exp"
@@ -240,7 +268,13 @@
   "bp' (PVar x) = {atom x}"
 | "bp' (PUnit) = {}"
 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
-thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
+
+thm exp_pat3_fv
+thm exp_pat3_inject
+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 =
@@ -257,7 +291,13 @@
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
+
+thm exp6_pat6_fv
+thm exp6_pat6_inject
+thm exp6_pat6_bn
+thm exp6_pat6_perm
+thm exp6_pat6_induct
+thm exp6_pat6_distinct
 
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)