--- a/src/HOL/String.thy Wed Oct 29 15:02:29 2014 +0100
+++ b/src/HOL/String.thy Wed Oct 29 15:07:53 2014 +0100
@@ -126,7 +126,6 @@
"_String" :: "str_position => string" ("_")
ML_file "Tools/string_syntax.ML"
-setup String_Syntax.setup
lemma UNIV_char:
"UNIV = image (split Char) (UNIV \<times> UNIV)"
--- a/src/HOL/Tools/string_syntax.ML Wed Oct 29 15:02:29 2014 +0100
+++ b/src/HOL/Tools/string_syntax.ML Wed Oct 29 15:07:53 2014 +0100
@@ -4,15 +4,9 @@
Concrete syntax for hex chars and strings.
*)
-signature STRING_SYNTAX =
-sig
- val setup: theory -> theory
-end;
-
-structure String_Syntax: STRING_SYNTAX =
+structure String_Syntax: sig end =
struct
-
(* nibble *)
val mk_nib =
@@ -91,12 +85,13 @@
(* theory setup *)
-val setup =
- Sign.parse_ast_translation
- [(@{syntax_const "_Char"}, K char_ast_tr),
- (@{syntax_const "_String"}, K string_ast_tr)] #>
- Sign.print_ast_translation
- [(@{const_syntax Char}, K char_ast_tr'),
- (@{syntax_const "_list"}, K list_ast_tr')];
+val _ =
+ Theory.setup
+ (Sign.parse_ast_translation
+ [(@{syntax_const "_Char"}, K char_ast_tr),
+ (@{syntax_const "_String"}, K string_ast_tr)] #>
+ Sign.print_ast_translation
+ [(@{const_syntax Char}, K char_ast_tr'),
+ (@{syntax_const "_list"}, K list_ast_tr')]);
end;