src/Tools/code/code_target.ML

--- a/src/Tools/code/code_target.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/Tools/code/code_target.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -23,7 +23,7 @@
   val add_pretty_list_string: string -> string -> string
     -> string -> string list -> theory -> theory;
   val add_pretty_char: string -> string -> string list -> theory -> theory
-  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string -> string
+  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
     -> string -> string -> theory -> theory;
   val add_pretty_message: string -> string -> string list -> string
     -> string -> string -> theory -> theory;
@@ -234,7 +234,7 @@
     else NONE
   end;
 
-fun implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit =
+fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
   let
     fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
           else if c = c_bit1 then 1
@@ -244,10 +244,9 @@
           else if c = c_min then
             if negative then SOME ~1 else NONE
           else error "Illegal numeral expression: illegal leading digit"
-      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
-          if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
-            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
-          else error "Illegal numeral expression: illegal bit shift operator"
+      | dest_numeral (t1 `$ t2) =
+          let val (n, b) = (dest_numeral t2, dest_bit t1)
+          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
       | dest_numeral _ = error "Illegal numeral expression: illegal constant";
   in dest_numeral #> the_default 0 end;
 
@@ -1825,11 +1824,11 @@
         | NONE => error "Illegal character expression";
   in (2, pretty) end;
 
-fun pretty_numeral unbounded negative c_bit0 c_bit1 c_pls c_min c_bit target =
+fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   let
     val mk_numeral = #pretty_numeral (pr_pretty target);
     fun pretty _ _ _ [(t, _)] =
-      (str o mk_numeral unbounded o implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit) t;
+      (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
   in (1, pretty) end;
 
 fun pretty_message c_char c_nibbles c_nil c_cons target =
@@ -2100,14 +2099,13 @@
     |> add_syntax_const target charr (SOME pr)
   end;
 
-fun add_pretty_numeral target unbounded negative number_of b0 b1 pls min bit thy =
+fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   let
-    val b0' = CodeName.const thy b0;
-    val b1' = CodeName.const thy b1;
     val pls' = CodeName.const thy pls;
     val min' = CodeName.const thy min;
-    val bit' = CodeName.const thy bit;
-    val pr = pretty_numeral unbounded negative b0' b1' pls' min' bit' target;
+    val bit0' = CodeName.const thy bit0;
+    val bit1' = CodeName.const thy bit1;
+    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
   in
     thy
     |> add_syntax_const target number_of (SOME pr)