diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      StateSpaceLocale.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -18,7 +17,7 @@
 
 locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
- and   "inject":: "'a \<Rightarrow> 'value"
+  and inject :: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
 
 lemma (in project_inject)