--- a/Nominal/Nominal2_Base.thy	Fri Jun 10 15:52:17 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 14 11:43:06 2011 +0100
@@ -2759,7 +2759,7 @@
   by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
 
 lemma at_base_class:
-  fixes sort_fun :: "'b \<Rightarrow>atom_sort"
+  fixes sort_fun :: "'b \<Rightarrow> atom_sort"
   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
   assumes atom_def: "\<And>a. atom a = Rep a"