# HG changeset patch
# User wenzelm
# Date 889456581 -3600
# Node ID d24168720303650e29a9daf47365115049571477
# Parent  580bf0f3ef799ae9317c945dd4b3772a87046b35
Symbol.explode;

diff -r 580bf0f3ef79 -r d24168720303 src/HOL/Integ/Bin.thy
--- 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 =
diff -r 580bf0f3ef79 -r d24168720303 src/HOLCF/domain/extender.ML
--- 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,
diff -r 580bf0f3ef79 -r d24168720303 src/HOLCF/domain/interface.ML
--- 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])
diff -r 580bf0f3ef79 -r d24168720303 src/HOLCF/domain/library.ML
--- 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);
diff -r 580bf0f3ef79 -r d24168720303 src/HOLCF/domain/syntax.ML
--- 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));
diff -r 580bf0f3ef79 -r d24168720303 src/ZF/ex/Bin.thy
--- 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 =