modernized setup;
authorwenzelm
Wed Oct 29 15:07:53 2014 +0100 (2014-10-29)
changeset 5882290a5e981af3e
parent 58821 11e226e8a095
child 58823 513268cb2178
modernized setup;
src/HOL/String.thy
src/HOL/Tools/string_syntax.ML
     1.1 --- a/src/HOL/String.thy	Wed Oct 29 15:02:29 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Oct 29 15:07:53 2014 +0100
     1.3 @@ -126,7 +126,6 @@
     1.4    "_String" :: "str_position => string"    ("_")
     1.5  
     1.6  ML_file "Tools/string_syntax.ML"
     1.7 -setup String_Syntax.setup
     1.8  
     1.9  lemma UNIV_char:
    1.10    "UNIV = image (split Char) (UNIV \<times> UNIV)"
     2.1 --- a/src/HOL/Tools/string_syntax.ML	Wed Oct 29 15:02:29 2014 +0100
     2.2 +++ b/src/HOL/Tools/string_syntax.ML	Wed Oct 29 15:07:53 2014 +0100
     2.3 @@ -4,15 +4,9 @@
     2.4  Concrete syntax for hex chars and strings.
     2.5  *)
     2.6  
     2.7 -signature STRING_SYNTAX =
     2.8 -sig
     2.9 -  val setup: theory -> theory
    2.10 -end;
    2.11 -
    2.12 -structure String_Syntax: STRING_SYNTAX =
    2.13 +structure String_Syntax: sig end =
    2.14  struct
    2.15  
    2.16 -
    2.17  (* nibble *)
    2.18  
    2.19  val mk_nib =
    2.20 @@ -91,12 +85,13 @@
    2.21  
    2.22  (* theory setup *)
    2.23  
    2.24 -val setup =
    2.25 -  Sign.parse_ast_translation
    2.26 -   [(@{syntax_const "_Char"}, K char_ast_tr),
    2.27 -    (@{syntax_const "_String"}, K string_ast_tr)] #>
    2.28 -  Sign.print_ast_translation
    2.29 -   [(@{const_syntax Char}, K char_ast_tr'),
    2.30 -    (@{syntax_const "_list"}, K list_ast_tr')];
    2.31 +val _ =
    2.32 +  Theory.setup
    2.33 +   (Sign.parse_ast_translation
    2.34 +     [(@{syntax_const "_Char"}, K char_ast_tr),
    2.35 +      (@{syntax_const "_String"}, K string_ast_tr)] #>
    2.36 +    Sign.print_ast_translation
    2.37 +     [(@{const_syntax Char}, K char_ast_tr'),
    2.38 +      (@{syntax_const "_list"}, K list_ast_tr')]);
    2.39  
    2.40  end;