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