# HG changeset patch
# User haftmann
# Date 1243950783 -7200
# Node ID 815426e7dd3bd40062e9dc2029d2ea4674f78a8f
# Parent  edf74583715a4e5a5e276ae15df48d24bcef60f8
tuned whitespace

diff -r edf74583715a -r 815426e7dd3b src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Tue Jun 02 10:04:03 2009 +0200
+++ b/src/HOL/Tools/numeral.ML	Tue Jun 02 15:53:03 2009 +0200
@@ -77,7 +77,7 @@
       (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
         o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
-    thy |>  Code_Target.add_syntax_const target number_of
+    thy |> Code_Target.add_syntax_const target number_of
       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
   end;