--- a/Quot/Nominal/Perm.thy	Wed Feb 24 15:13:22 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 15:36:07 2010 +0100
@@ -109,13 +109,19 @@
       (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)
-    fun tac ctxt perm_thms =
+    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);
   in
-    Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy'
+  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)
   end
 
 *}