--- 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