tuned ML bindings;

--- a/src/HOL/ex/Binary.thy	Fri Aug 10 17:10:09 2007 +0200
+++ b/src/HOL/ex/Binary.thy	Fri Aug 10 18:21:25 2007 +0200
@@ -21,6 +21,8 @@
   unfolding bit_def by simp_all
 
 ML {*
+structure Binary =
+struct
   fun dest_bit (Const ("False", _)) = 0
     | dest_bit (Const ("True", _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
@@ -42,6 +44,7 @@
         else
           let val (q, r) = IntInf.divMod (n, 2)
           in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
+end
 *}
 
 
@@ -124,7 +127,7 @@
   fun binary_proc proc ss ct =
     (case Thm.term_of ct of
       _ $ t $ u =>
-      (case try (pairself (`dest_binary)) (t, u) of
+      (case try (pairself (`Binary.dest_binary)) (t, u) of
         SOME args => proc (Simplifier.the_context ss) args
       | NONE => NONE)
     | _ => NONE);
@@ -133,34 +136,34 @@
 val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = n - m in
     if k >= 0 then
-      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
+      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
     else
       SOME (@{thm binary_less_eq(2)} OF
-        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
+        [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
   end);
 
 val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = m - n in
     if k >= 0 then
-      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
+      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
     else
       SOME (@{thm binary_less(2)} OF
-        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
+        [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
   end);
 
 val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = m - n in
     if k >= 0 then
-      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
+      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
     else
-      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
+      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
   end);
 
 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   if n = 0 then NONE
   else
     let val (k, l) = IntInf.divMod (m, n)
-    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
+    in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
 
 end;
 *}
@@ -199,7 +202,7 @@
       let
         val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
         val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
-      in syntax_consts (mk_binary n) end
+      in syntax_consts (Binary.mk_binary n) end
   | binary_tr ts = raise TERM ("binary_tr", ts);
 
 in [("_Binary", binary_tr)] end