authentic syntax for number_of
authorhaftmann
Wed Dec 13 15:45:33 2006 +0100 (2006-12-13)
changeset 218217fa19d17f488
parent 21820 2f2b6a965ccc
child 21822 5a279c9138b6
authentic syntax for number_of
src/HOL/Tools/numeral_syntax.ML
     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;