--- a/Nominal/Ex/Classical.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/Classical.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -7,7 +7,7 @@
 atom_decl name
 atom_decl coname
 
-declare [[STEPS = 9]]
+declare [[STEPS = 21]]
 
 nominal_datatype trm =
    Ax "name" "coname"
@@ -18,17 +18,17 @@
 |  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
-thm alpha_trm_raw.intros[no_vars]
+thm distinct
+thm induct
+thm exhaust
+thm fv_defs
+thm bn_defs
+thm perm_simps
+thm eq_iff
+thm fv_bn_eqvt
+thm size_eqvt
 
-(*
-thm trm.fv
-thm trm.eq_iff
-thm trm.bn
-thm trm.perm
-thm trm.induct
-thm trm.distinct
-thm trm.fv[simplified trm.supp]
-*)
+
 
 
 end

--- a/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype tkind =
   KStar
@@ -88,72 +88,15 @@
 (* can lift *)
 
 thm distinct
+thm induct
+thm exhaust
 thm fv_defs
-thm alpha_bn_imps alpha_equivp
-
-thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts
+thm bn_defs
 thm perm_simps
-thm perm_laws
-thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)
-
 thm eq_iff
-thm eq_iff_simps
-
-ML {*
-  val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co},
-              @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars},
-              @{typ tvars}, @{typ cvars}]
-*}
-
-
-ML {*
-  val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
-*}
-
-ML {* 
-  val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.induct})
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
-*}
+thm fv_bn_eqvt
+thm size_eqvt
 
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
-*}
-
-ML {*
-  val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
-*}
-
-ML {*
-  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
-    prod.cases}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
-*}
 
 
 

--- a/Nominal/Ex/Lambda.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -3,7 +3,7 @@
 begin
 
 atom_decl name
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 class s1
 class s2
@@ -14,88 +14,16 @@
 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
 | Lam x::"name" l::"('a, 'b) lam"  bind x in l
 
-term Var_raw
-term Var
-term App_raw
-term App
-thm Var_def App_def Lam_def
-term abs_lam
-
 thm distinct
-thm lam_raw.inducts
-thm lam_raw.exhaust
+thm induct
+thm exhaust
 thm fv_defs
 thm bn_defs
 thm perm_simps
-thm perm_laws
-thm lam_raw.size
 thm eq_iff
-thm eq_iff_simps
-thm fv_eqvt
-thm bn_eqvt
+thm fv_bn_eqvt
 thm size_eqvt
 
-ML {*
-  val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}]
-*}
-
-ML {*
-  val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
-*}
-
-ML {*
-  val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
-*}
-
-ML {*
-  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
-    prod.cases}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps}
-*}
-
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
-*}
-
-
-
-thm eq_iff
 
 thm lam.fv
 thm lam.supp

--- a/Nominal/Ex/SingleLet.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype singlelet: trm  =
   Var "name"
@@ -22,86 +22,17 @@
   "bn (As x y t) = {atom x}"
 
 
-text {* can lift *}
-
 thm distinct
-thm trm_raw_assg_raw.inducts
-thm trm_raw.exhaust
-thm assg_raw.exhaust
+thm induct
+thm exhaust
 thm fv_defs
 thm bn_defs
 thm perm_simps
-thm perm_laws
-thm trm_raw_assg_raw.size(9 - 16)
 thm eq_iff
-thm eq_iff_simps
-thm bn_defs
-thm fv_eqvt
-thm bn_eqvt
+thm fv_bn_eqvt
 thm size_eqvt
 
 
-ML {*
-  val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct})
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw.exhaust}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms assg_raw.exhaust}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_defs}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-ML {*
-  val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws}
-*}
-
-ML {*
-  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
-    prod.cases}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps)  @{thms eq_iff}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt}
-*}
-
 
 
 

--- a/Nominal/Ex/TypeSchemes.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -6,22 +6,22 @@
 
 atom_decl name
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind_res xs in ty
+  All xs::"name fset" ty::"ty" bind (res) xs in ty
+
 
 nominal_datatype ty2 =
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-instance ty2 :: pt sorry
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind_res xs in ty
+  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]

--- a/Nominal/NewParser.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -471,24 +471,50 @@
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
+
+  (* lifting of the theorems *)
+  val _ = warning "Lifting of Theorems"
+  
+  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases} 
+
+  val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
+    if get_STEPS lthy > 20
+    then 
+      lthy9a    
+      |> lift_thms qtys [] alpha_distincts  
+      ||>> lift_thms qtys eq_iff_simps alpha_eq_iff       
+      ||>> lift_thms qtys [] raw_fv_defs
+      ||>> lift_thms qtys [] raw_bn_defs
+      ||>> lift_thms qtys [] raw_perm_simps
+      ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+    else raise TEST lthy9a
+
+  val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = 
+    if get_STEPS lthy > 20
+    then
+      lthyA 
+      |> lift_thms qtys [] raw_size_eqvt
+      ||>> lift_thms qtys [] [raw_induct_thm]
+      ||>> lift_thms qtys [] raw_exhaust_thms
+    else raise TEST lthyA
+
   
   (* temporary theorem bindings *)
-  val (_, lthy9') = lthy9a
-     |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
-     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
-     ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
-     ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
-     ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) 
-     ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
-     ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
-     ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
-     ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms)
-     ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) 
-     ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt)      
-     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)      
+  val (_, lthy9') = lthyB
+     |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) 
+     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs)
+     ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) 
+     ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) 
+     ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) 
+     ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) 
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt)
+     ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) 
+     ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts)
+     
 
   val _ = 
-    if get_STEPS lthy > 20
+    if get_STEPS lthy > 21
     then true else raise TEST lthy9'
   
   (* old stuff *)
@@ -553,7 +579,7 @@
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) [];
-  val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys [] raw_induct_thm);
+  val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13)));
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =
@@ -563,24 +589,24 @@
     [Rule_Cases.name constr_names q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-  val q_perm = map (lift_thm lthy14 qtys []) raw_perm_simps;
+  val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14);
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
-  val q_fv = map (lift_thm lthy15 qtys []) raw_fv_defs;
+  val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15);
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm lthy16 qtys []) raw_bn_defs;
+  val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16);
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
   val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
-  val q_eq_iff_pre0 = map (lift_thm lthy17 qtys []) eq_iff_unfolded1;
+  val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17);
   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val q_dis = map (lift_thm lthy18 qtys []) alpha_distincts;
+  val q_dis = fst (lift_thms qtys [] alpha_distincts lthy18);
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm lthy19 qtys []) (raw_bn_eqvt @ raw_fv_eqvt);
+  val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";

--- a/Nominal/nominal_dt_quot.ML	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Wed Aug 25 22:55:42 2010 +0800
@@ -19,7 +19,7 @@
   val define_qsizes: typ list -> string list -> (string * sort) list -> 
     (string * term * mixfix) list -> local_theory -> local_theory
 
-  val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm
+  val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -49,8 +49,6 @@
 (* defines the quotient permutations and proves pt-class *)
 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
 let
-  val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys))
-
   val lthy1 = 
     lthy
     |> Local_Theory.exit_global
@@ -122,12 +120,12 @@
   Thm.rename_boundvars trm trm' th
 end
 
-fun lift_thm ctxt qtys simps thm =
-  thm
-  |> Quotient_Tacs.lifted ctxt qtys simps
-  |> unraw_bounds_thm
-  |> unraw_vars_thm
-  |> Drule.zero_var_indexes
+fun lift_thms qtys simps thms ctxt =
+  (map (Quotient_Tacs.lifted ctxt qtys simps
+        #> unraw_bounds_thm
+        #> unraw_vars_thm
+        #> Drule.zero_var_indexes) thms, ctxt)
+
 
 end (* structure *)