diff -r 60f7fb56f8cd -r 2d62b637fa80 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -16,7 +16,7 @@
 concrete values.*}
 
 
-locale project_inject =
+class_locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
  and   "inject":: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"