# 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 \ 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;