src/HOL/Tools/numeral_syntax.ML
changeset 21821 7fa19d17f488
parent 21789 c4f6bb392030
child 22997 d4f3b015b50b
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Dec 13 15:45:31 2006 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Dec 13 15:45:33 2006 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4  structure NumeralSyntax: NUMERAL_SYNTAX =
     1.5  struct
     1.6  
     1.7 -
     1.8  (* parse translation *)
     1.9  
    1.10  local
    1.11 @@ -90,6 +89,6 @@
    1.12  
    1.13  val setup =
    1.14    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.15 -  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
    1.16 +  Theory.add_trfunsT [("\\<^const>Numeral.number_of", numeral_tr')];
    1.17  
    1.18  end;