--- a/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:08:25 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:10:01 2010 +0100
@@ -15,15 +15,14 @@
(* nibble *)
-val nib_prefix = "String.nibble.";
-
val mk_nib =
- Syntax.Constant o unprefix nib_prefix o
+ Syntax.Constant o prefix Syntax.constN o
fst o Term.dest_Const o HOLogic.mk_nibble;
-fun dest_nib (Syntax.Constant c) =
- HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
- handle TERM _ => raise Match;
+fun dest_nib (Syntax.Constant s) =
+ (case try (unprefix Syntax.constN) s of
+ NONE => raise Match
+ | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
(* char *)