--- a/Nominal/Atoms.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Atoms.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -65,7 +65,7 @@
 
 lemma sort_of_atom_name: 
   shows "sort_of (atom (a::name)) = Sort ''name'' []"
-  unfolding atom_name_def using Rep_name by simp
+  by (simp add: atom_name_def Rep_name[simplified])
 
 text {* Custom syntax for concrete atoms of type at *}
 
@@ -104,11 +104,10 @@
 
 atom_decl name2
 
-lemma sort_of_atom_name2:
-  "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"
-unfolding atom_name2_def 
-using Rep_name2 
-by simp
+lemma 
+  "sort_of (atom (a::name2)) \<noteq> sort_of (atom (b::name))"
+by (simp add: sort_of_atom_name)
+
 
 text {* example swappings *}
 lemma

--- a/Nominal/Ex/Classical.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -9,7 +9,7 @@
 
 nominal_datatype trm =
   Ax "name" "coname"
-| Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2  
+| Cut c::"coname" t1::"trm" n::"name" t2::"trm"             bind n in t1, bind c in t2  
      ("Cut <_>._ '(_')._" [100,100,100,100] 100)
 | NotR n::"name" t::"trm" "coname"                            bind n in t
      ("NotR '(_')._ _" [100,100,100] 100)
@@ -46,7 +46,7 @@
 thm trm.supp
 thm trm.supp[simplified]
 
-nominal_primrec 
+nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *)
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
@@ -68,6 +68,8 @@
   apply(simp only: eqvt_def)
   apply(simp only: crename_graph_def)
   apply (rule, perm_simp, rule)
+  (*apply(erule crename_graph.induct)
+  apply(simp add: trm.fresh)*)
   apply(rule TrueI)
   -- "covered all cases"
   apply(case_tac x)
@@ -96,8 +98,21 @@
   apply(metis)  
   apply(simp add: fresh_star_def)
   apply(metis)
-  -- "clashes"
+  -- "compatibility"
   apply(simp_all)
+  apply(rule conjI)
+  apply(erule conjE)+
+  apply(erule Abs_lst1_fcb)
+  apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
+  apply(erule fresh_eqvt_at)
+  apply(simp add: finite_supp)
+  apply(simp add: fresh_Pair fresh_at_base(1))
+  apply(drule sym)
+  apply(drule sym)
+  apply(drule sym)
+  apply(drule sym)
+  apply(simp add: eqvt_at_def swap_fresh_fresh)
   oops
 
 end

--- a/Nominal/Ex/Lambda.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -18,7 +18,7 @@
 val test:((Proof.context -> Method.method) context_parser) =
 Scan.succeed (fn ctxt =>
  let
-   val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph"
+   val _ = Inductive.the_inductive ctxt "local.frees_lst_graph"
  in 
    Method.SIMPLE_METHOD' (K all_tac)
  end)

--- a/Nominal/Nominal2_Base.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -2577,9 +2577,13 @@
   by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
 
 lemma fresh_at_base: 
-  shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
-  unfolding fresh_def by (simp add: supp_at_base)
-
+  shows  "sort_of a \<noteq> sort_of (atom b) \<Longrightarrow> a \<sharp> b"
+  and "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
+  unfolding fresh_def 
+  apply(simp_all add: supp_at_base)
+  apply(metis)
+  done
+  
 lemma fresh_atom_at_base: 
   fixes b::"'a::at_base"
   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
@@ -2684,7 +2688,6 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
-
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -2841,13 +2844,22 @@
     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
 qed
 
+lemma at_class_sort:
+  fixes s :: atom_sort
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  fixes a::"'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a = s}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  shows "sort_of (atom a) = s"
+  using atom_def type
+  unfolding type_definition_def by simp
+
+
 setup {* Sign.add_const_constraint
   (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
 setup {* Sign.add_const_constraint
   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
 
-
-
 section {* The freshness lemma according to Andy Pitts *}
 
 lemma freshness_lemma:

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