--- a/src/HOL/Integ/Bin.thy Wed Mar 17 17:18:54 1999 +0100
+++ b/src/HOL/Integ/Bin.thy Wed Mar 17 17:19:18 1999 +0100
@@ -101,12 +101,11 @@
(** Concrete syntax for integers **)
local
- open Syntax;
(* Bits *)
- fun mk_bit 0 = const "False"
- | mk_bit 1 = const "True"
+ fun mk_bit 0 = Syntax.const "False"
+ | mk_bit 1 = Syntax.const "True"
| mk_bit _ = sys_error "mk_bit";
fun dest_bit (Const ("False", _)) = 0
@@ -132,16 +131,16 @@
| bin_of ~1 = [~1]
| bin_of n = (n mod 2) :: bin_of (n div 2);
- fun term_of [] = const "Bin.bin.Pls"
- | term_of [~1] = const "Bin.bin.Min"
- | term_of (b :: bs) = const "Bin.bin.op BIT" $ term_of bs $ mk_bit b;
+ fun term_of [] = Syntax.const "Bin.bin.Pls"
+ | term_of [~1] = Syntax.const "Bin.bin.Min"
+ | term_of (b :: bs) = Syntax.const "Bin.bin.op BIT" $ term_of bs $ mk_bit b;
in
term_of (bin_of (sign * (#1 (read_int digs))))
end;
fun dest_bin tm =
let
- (*We consider both "spellings", since Min might be declared elsewhere*)
+ (*we consider both "spellings", since Min might be declared elsewhere*)
fun bin_of (Const ("Pls", _)) = []
| bin_of (Const ("bin.Pls", _)) = []
| bin_of (Const ("Min", _)) = [~1]
@@ -167,11 +166,12 @@
(* translation of integer constant tokens to and from binary *)
fun int_tr (*"_Int"*) [t as Free (str, _)] =
- (const "integ_of" $
+ (Syntax.const "integ_of" $
(mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
- fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
+ fun int_tr' (*"integ_of"*) [t] =
+ Syntax.const "_Int" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin t))
| int_tr' (*"integ_of"*) _ = raise Match;
in
val parse_translation = [("_Int", int_tr)];