--- a/src/HOL/Modelcheck/MuckeExample1.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Modelcheck/MuckeExample1.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -11,8 +11,7 @@
 types
   state = "bool * bool * bool"
 
-constdefs
-  INIT :: "state pred"
+definition INIT :: "state pred" where
   "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
   N    :: "[state,state] => bool"
   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));