# HG changeset patch
# User wenzelm
# Date 1414591673 -3600
# Node ID 90a5e981af3ed8483fb46e7264168f522c7da4c6
# Parent  11e226e8a095499df5b7e11cba465e5c107a02a1
modernized setup;

diff -r 11e226e8a095 -r 90a5e981af3e src/HOL/String.thy
--- 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)"
diff -r 11e226e8a095 -r 90a5e981af3e src/HOL/Tools/string_syntax.ML
--- 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;