diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Char_ord.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -32,8 +32,8 @@
   "nibble_to_int NibbleF = 15"
 
 definition
-  int_to_nibble :: "int \<Rightarrow> nibble"
-  "int_to_nibble x \<equiv> (let y = x mod 16 in
+  int_to_nibble :: "int \<Rightarrow> nibble" where
+  "int_to_nibble x = (let y = x mod 16 in
     if y = 0 then Nibble0 else
     if y = 1 then Nibble1 else
     if y = 2 then Nibble2 else