--- a/Nominal/nominal_atoms.ML	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/nominal_atoms.ML	Thu Jun 23 22:21:43 2011 +0100
@@ -15,6 +15,8 @@
 structure Atom_Decl :> ATOM_DECL =
 struct
 
+val simp_attr = Attrib.internal (K Simplifier.simp_add)
+
 fun atom_decl_set (str : string) : term =
   let
     val a = Free ("a", @{typ atom});
@@ -48,6 +50,8 @@
         (mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
     val atom_def_name =
       Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
+    val sort_thm_name =
+      Binding.prefix_name "atom_" (Binding.suffix_name "_sort" name);
     val permute_def_name =
       Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
 
@@ -62,8 +66,10 @@
     val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
     val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
+    val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
     val thy = lthy
-      |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))
+      |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm]))
+      |> Class.prove_instantiation_instance (K (rtac class_thm 1))
       |> Local_Theory.exit_global;
   in
     thy