src/HOL/Tools/numeral_syntax.ML
changeset 24712 64ed05609568
parent 24630 351a308ab58d
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val setup =
     1.7 -  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
     1.8 -  Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
     1.9 +  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.10 +  Sign.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
    1.11  
    1.12  end;