changeset 15570 | 8d8c70b41bab |
parent 15531 | 08c8dad8e399 |
child 15656 | 988f91b9c4ef |
--- 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