--- a/Quot/Nominal/Perm.thy	Wed Feb 24 23:25:30 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Thu Feb 25 07:05:52 2010 +0100
@@ -98,24 +98,23 @@
     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 _ (_, simps) =
+    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);
+    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_ldef, (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
 
 *}