1.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -408,7 +408,7 @@
     1.4    in bin_of n end;
     1.5  
     1.6  fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
     1.7 -      mk_bintype (valOf (Int.fromString str))
     1.8 +      mk_bintype (the (Int.fromString str))
     1.9    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    1.10  
    1.11  in [("_NumeralType", numeral_tr)] end;