--- a/Quot/Nominal/LFex.thy	Wed Feb 24 15:39:17 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 17:42:37 2010 +0100
@@ -20,6 +20,7 @@
 
 
 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+print_theorems
 
 local_setup {*
   snd o define_fv_alpha "LFex.rkind"
@@ -117,29 +118,11 @@
 thm rkind_rty_rtrm.inducts
 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
 
-instantiation kind and ty and trm :: pt
-begin
-
-quotient_definition
-  "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
-is
-  "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
-
-quotient_definition
-  "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
-is
-  "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
-
-quotient_definition
-  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
-is
-  "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
-
-instance by default (simp_all add:
-  permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
-  permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] 
+  [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}),
+   ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}),
+   ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})]
+  @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *}
 
 (*
 Lifts, but slow and not needed?.

--- a/Quot/Nominal/Perm.thy	Wed Feb 24 15:39:17 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 17:42:37 2010 +0100
@@ -112,20 +112,34 @@
     val perms_name = space_implode "_" perm_names'
     val perms_zero_bind = Binding.name (perms_name ^ "_zero")
     val perms_append_bind = Binding.name (perms_name ^ "_append")
-    fun tac _ perm_thms =
-      (Class.intro_classes_tac []) THEN (ALLGOALS (
-        simp_tac (HOL_ss addsimps perm_thms
-      )));
-    fun morphism phi = map (Morphism.thm phi);
+    fun tac _ (_, simps) =
+      (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));
+    fun morphism phi (dfs, simps) = (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
   in
   lthy'
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
-  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms)
+  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms))
   end
 
 *}
 
+ML {*
+fun define_lifted_perms full_tnames name_term_pairs thms thy =
+let
+  val lthy =
+    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
+  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+    (ALLGOALS (resolve_tac lifted_thms))
+  val lthy'' = Class.prove_instantiation_instance tac lthy'
+in
+  Local_Theory.exit_global lthy''
+end
+*}
+
 (* Test
 atom_decl name
 

--- a/Quot/Nominal/Terms.thy	Wed Feb 24 15:39:17 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 17:42:37 2010 +0100
@@ -150,18 +150,8 @@
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 
-instantiation trm1 and bp :: pt
-begin
-
-quotient_definition
-  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
-
-instance by default 
-  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
+  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
 
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]