diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -216,10 +216,10 @@
 
 text"This is still a bit rough, especially the proof."
 
-constdefs
- cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "cor P Q == if P then True else Q"
- cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+
+definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "cand P Q == if P then Q else False"
 
 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
@@ -481,7 +481,7 @@
 
 subsection "Storage allocation"
 
-constdefs new :: "'a set \<Rightarrow> 'a"
+definition new :: "'a set \<Rightarrow> 'a" where
 "new A == SOME a. a \<notin> A"