diff -r 1b3115d1a8df -r 8d8c70b41bab src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/List.thy	Thu Mar 03 12:43:01 2005 +0100
@@ -2127,7 +2127,7 @@
     (let val c = chr (dest_nibble c1 * 16 + dest_nibble c2)
      in if Symbol.is_printable c then SOME (gr, Pretty.quote (Pretty.str c))
        else NONE
-     end handle LIST _ => NONE | Match => NONE)
+     end handle Fail _ => NONE | Match => NONE)
   | char_codegen thy gr dep b _ = NONE;
 
 in