1.1 --- a/src/HOL/Int.thy	Sat Feb 13 23:16:06 2010 +0100
     1.2 +++ b/src/HOL/Int.thy	Sat Feb 13 23:24:57 2010 +0100
     1.3 @@ -604,7 +604,7 @@
     1.4    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
     1.5  
     1.6  use "Tools/numeral_syntax.ML"
     1.7 -setup NumeralSyntax.setup
     1.8 +setup Numeral_Syntax.setup
     1.9  
    1.10  abbreviation
    1.11    "Numeral0 \<equiv> number_of Pls"

     2.1 --- a/src/HOL/RealPow.thy	Sat Feb 13 23:16:06 2010 +0100
     2.2 +++ b/src/HOL/RealPow.thy	Sat Feb 13 23:24:57 2010 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
     2.5  
     2.6  use "Tools/float_syntax.ML"
     2.7 -setup FloatSyntax.setup
     2.8 +setup Float_Syntax.setup
     2.9  
    2.10  text{* Test: *}
    2.11  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"

     3.1 --- a/src/HOL/String.thy	Sat Feb 13 23:16:06 2010 +0100
     3.2 +++ b/src/HOL/String.thy	Sat Feb 13 23:24:57 2010 +0100
     3.3 @@ -79,7 +79,7 @@
     3.4    "_String" :: "xstr => string"    ("_")
     3.5  
     3.6  use "Tools/string_syntax.ML"
     3.7 -setup StringSyntax.setup
     3.8 +setup String_Syntax.setup
     3.9  
    3.10  definition chars :: string where
    3.11    "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,

     4.1 --- a/src/HOL/Tools/float_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
     4.2 +++ b/src/HOL/Tools/float_syntax.ML	Sat Feb 13 23:24:57 2010 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4    val setup: theory -> theory
     4.5  end;
     4.6  
     4.7 -structure FloatSyntax: FLOAT_SYNTAX =
     4.8 +structure Float_Syntax: FLOAT_SYNTAX =
     4.9  struct
    4.10  
    4.11  (* parse translation *)

     5.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
     5.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sat Feb 13 23:24:57 2010 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4    val setup: theory -> theory
     5.5  end;
     5.6  
     5.7 -structure NumeralSyntax: NUMERAL_SYNTAX =
     5.8 +structure Numeral_Syntax: NUMERAL_SYNTAX =
     5.9  struct
    5.10  
    5.11  (* parse translation *)

     6.1 --- a/src/HOL/Tools/string_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
     6.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat Feb 13 23:24:57 2010 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4    val setup: theory -> theory
     6.5  end;
     6.6  
     6.7 -structure StringSyntax: STRING_SYNTAX =
     6.8 +structure String_Syntax: STRING_SYNTAX =
     6.9  struct
    6.10  
    6.11  
    6.12 @@ -19,7 +19,7 @@
    6.13  
    6.14  val mk_nib =
    6.15    Syntax.Constant o unprefix nib_prefix o
    6.16 -  fst o Term.dest_Const o HOLogic.mk_nibble;
    6.17 +    fst o Term.dest_Const o HOLogic.mk_nibble;
    6.18  
    6.19  fun dest_nib (Syntax.Constant c) =
    6.20    HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))

     7.1 --- a/src/ZF/Bin.thy	Sat Feb 13 23:16:06 2010 +0100
     7.2 +++ b/src/ZF/Bin.thy	Sat Feb 13 23:24:57 2010 +0100
     7.3 @@ -105,7 +105,7 @@
     7.4    "_Int"    :: "xnum => i"        ("_")
     7.5  
     7.6  use "Tools/numeral_syntax.ML"
     7.7 -setup NumeralSyntax.setup
     7.8 +setup Numeral_Syntax.setup
     7.9  
    7.10  
    7.11  declare bin.intros [simp,TC]

     8.1 --- a/src/ZF/Tools/numeral_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
     8.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Sat Feb 13 23:24:57 2010 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4    val setup: theory -> theory
     8.5  end;
     8.6  
     8.7 -structure NumeralSyntax: NUMERAL_SYNTAX =
     8.8 +structure Numeral_Syntax: NUMERAL_SYNTAX =
     8.9  struct
    8.10  
    8.11  (* bits *)

     9.1 --- a/src/ZF/int_arith.ML	Sat Feb 13 23:16:06 2010 +0100
     9.2 +++ b/src/ZF/int_arith.ML	Sat Feb 13 23:24:57 2010 +0100
     9.3 @@ -22,7 +22,7 @@
     9.4      fun term_of [] = @{term Pls}
     9.5        | term_of [~1] = @{term Min}
     9.6        | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
     9.7 -  in term_of (NumeralSyntax.make_binary i) end;
     9.8 +  in term_of (Numeral_Syntax.make_binary i) end;
     9.9  
    9.10  fun dest_bin tm =
    9.11    let
    9.12 @@ -30,7 +30,7 @@
    9.13        | bin_of @{term Min} = [~1]
    9.14        | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
    9.15        | bin_of _ = sys_error "dest_bin";
    9.16 -  in NumeralSyntax.dest_binary (bin_of tm) end;
    9.17 +  in Numeral_Syntax.dest_binary (bin_of tm) end;
    9.18  
    9.19  
    9.20  (*Utilities*)