src/HOL/Tools/numeral.ML
changeset 28708 a1a436f09ec6
parent 28663 bd8438543bf2
child 31056 01ac77eb660b
     1.1 --- a/src/HOL/Tools/numeral.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/HOL/Tools/numeral.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4                in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
     1.5            | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
     1.6        in dest_num end;
     1.7 -    fun pretty _ naming thm _ _ _ [(t, _)] =
     1.8 +    fun pretty _ naming thm _ _ [(t, _)] =
     1.9        (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
    1.10    in
    1.11      thy