--- a/src/HOL/Tools/string_syntax.ML Wed May 06 16:01:05 2009 +0200
+++ b/src/HOL/Tools/string_syntax.ML Wed May 06 16:01:06 2009 +0200
@@ -15,12 +15,14 @@
(* nibble *)
+val nib_prefix = "String.nibble.";
+
val mk_nib =
- Syntax.Constant o unprefix "List.nibble." o
+ Syntax.Constant o unprefix nib_prefix o
fst o Term.dest_Const o HOLogic.mk_nibble;
fun dest_nib (Syntax.Constant c) =
- HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT))
+ HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
handle TERM _ => raise Match;