--- a/src/HOL/Integ/Bin.thy Mon Mar 09 16:15:24 1998 +0100
+++ b/src/HOL/Integ/Bin.thy Mon Mar 09 16:16:21 1998 +0100
@@ -112,7 +112,7 @@
fun mk_bin str =
let
val (sign, digs) =
- (case explode str of
+ (case Symbol.explode str of
"#" :: "~" :: cs => (~1, cs)
| "#" :: cs => (1, cs)
| _ => raise ERROR);
@@ -127,7 +127,7 @@
| term_of [~1] = const "MinusSign"
| term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
in
- term_of (bin_of (sign * (#1 (scan_int digs))))
+ term_of (bin_of (sign * (#1 (read_int digs))))
end;
fun dest_bin tm =
--- a/src/HOLCF/domain/extender.ML Mon Mar 09 16:15:24 1998 +0100
+++ b/src/HOLCF/domain/extender.ML Mon Mar 09 16:16:21 1998 +0100
@@ -85,9 +85,9 @@
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
val dts = map (Type o fst) eqs';
fun strip ss = drop (find_index_eq "'" ss +1, ss);
- fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
- | typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id))))
- | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
+ fun typid (Type (id,_) ) = hd (Symbol.explode (Sign.base_name id))
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode (Sign.base_name id))))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode (Sign.base_name id)));
fun cons cons' = (map (fn (con,syn,args) =>
((Syntax.const_name con syn),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
--- a/src/HOLCF/domain/interface.ML Mon Mar 09 16:15:24 1998 +0100
+++ b/src/HOLCF/domain/interface.ML Mon Mar 09 16:16:21 1998 +0100
@@ -14,7 +14,7 @@
fun get dname name = "get_thm thy " ^ quote (dname^"."^name);
fun gen_vals dname name = "val "^ name ^ " = get_thm" ^
- (if hd (rev (explode name)) = "s" then "s" else "")^
+ (if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
" thy " ^ quote (dname^"."^name)^";";
fun gen_vall name l = "val "^name^" = "^ mk_list l^";";
val rews = "iso_rews @ when_rews @\n\
@@ -109,7 +109,7 @@
| esc ("[" ::xs) = "{"::esc xs
| esc ("]" ::xs) = "}"::esc xs
| esc (x ::xs) = x ::esc xs
- in implode (esc (explode s)) end;
+ in implode (esc (Symbol.explode s)) end;
val tvar = (type_var' ^^
optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
fun type_args l = (tvar >> (fn x => [x])
--- a/src/HOLCF/domain/library.ML Mon Mar 09 16:15:24 1998 +0100
+++ b/src/HOLCF/domain/library.ML Mon Mar 09 16:16:21 1998 +0100
@@ -50,9 +50,9 @@
| strip ["'"] = []
| strip (c :: cs) = c :: strip cs
| strip [] = [];
-in implode o strip o explode end;
+in implode o strip o Symbol.explode end;
-fun extern_name con = case explode con of
+fun extern_name con = case Symbol.explode con of
("o"::"p"::" "::rest) => implode rest
| _ => con;
fun dis_name con = "is_"^ (extern_name con);
--- a/src/HOLCF/domain/syntax.ML Mon Mar 09 16:15:24 1998 +0100
+++ b/src/HOLCF/domain/syntax.ML Mon Mar 09 16:16:21 1998 +0100
@@ -42,7 +42,7 @@
fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
else c::esc cs
| esc [] = []
- in implode o esc o explode end;
+ in implode o esc o Symbol.explode end;
fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
Mixfix(escape ("is_" ^ con), [], max_pri));
--- a/src/ZF/ex/Bin.thy Mon Mar 09 16:15:24 1998 +0100
+++ b/src/ZF/ex/Bin.thy Mon Mar 09 16:16:21 1998 +0100
@@ -117,7 +117,7 @@
fun mk_bin str =
let
val (sign, digs) =
- (case explode str of
+ (case Symbol.explode str of
"#" :: "~" :: cs => (~1, cs)
| "#" :: cs => (1, cs)
| _ => raise ERROR);
@@ -132,7 +132,7 @@
| term_of [~1] = const "Minus"
| term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
in
- term_of (bin_of (sign * (#1 (scan_int digs))))
+ term_of (bin_of (sign * (#1 (read_int digs))))
end;
fun dest_bin tm =