src/HOL/ex/Binary.thy

     "bit n False = 2 * n"
     "bit n True = 2 * n + 1"
   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]);
 
   fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0

     | mk_binary n =
         if n < 0 then raise TERM ("mk_binary", [])
         else
           let val (q, r) = IntInf.divMod (n, 2)
           in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
+end
 *}
 
 
 subsection {* Direct operations -- plain normalization *}
 

     Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
 
   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);
 in
 
 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;
 *}
 
 simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}

 
 fun binary_tr [Const (num, _)] =
       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
 *}