diff -r 1a0c129bb2e0 -r b1fd1d756e20 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:19:58 2010 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:55:16 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      StateFun.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -34,12 +33,12 @@
 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
   by (rule refl)
 
-constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
-"lookup destr n s \<equiv> destr (s n)"
+definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+  where "lookup destr n s = destr (s n)"
 
-constdefs update:: 
+definition update::
   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
-"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
+  where "update destr constr n f s = s(n := constr (f (destr (s n))))"
 
 lemma lookup_update_same:
   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) =