--- a/Nominal/Perm.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Perm.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -13,13 +13,11 @@
 let
   val perm_types = map fastype_of perm_frees;
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
   val gl =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) => HOLogic.mk_eq
-          (perm $ @{term "0 :: perm"} $ Free (x, T),
-           Free (x, T)))
-       (perm_frees ~~
-        map body_type perm_types ~~ perm_indnames)));
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,
@@ -38,15 +36,13 @@
   val pi2 = Free ("pi2", @{typ perm});
   val perm_types = map fastype_of perm_frees
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (
+      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
+      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
   val gl =
     (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) =>
-          let
-            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-          in HOLogic.mk_eq (lhs, rhs)
-          end)
-        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,
@@ -102,30 +98,43 @@
     val lthy =
       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
     (* TODO: Use the version of prmrec that gives the names explicitely. *)
-    val ((_, perm_ldef), lthy') =
+    val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
-    val perm_frees =
-      (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
     val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
     val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
     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, fvs) =
+      (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   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), perm_frees)
   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