# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308048186 -3600
# Node ID 5165f4552cd58ade8b0fa3740bc7668359e3f9dc
# Parent  1d43d30e44c958a6c1891f711998809d0e8649ed
tuned

diff -r 1d43d30e44c9 -r 5165f4552cd5 Nominal/Nominal2_Base.thy
--- 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"