Symbol.explode;
authorwenzelm
Mon Mar 09 16:16:21 1998 +0100 (1998-03-09)
changeset 4709d24168720303
parent 4708 580bf0f3ef79
child 4710 05e57f1879ee
Symbol.explode;
src/HOL/Integ/Bin.thy
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/ZF/ex/Bin.thy
     1.1 --- a/src/HOL/Integ/Bin.thy	Mon Mar 09 16:15:24 1998 +0100
     1.2 +++ b/src/HOL/Integ/Bin.thy	Mon Mar 09 16:16:21 1998 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4    fun mk_bin str =
     1.5      let
     1.6        val (sign, digs) =
     1.7 -        (case explode str of
     1.8 +        (case Symbol.explode str of
     1.9            "#" :: "~" :: cs => (~1, cs)
    1.10          | "#" :: cs => (1, cs)
    1.11          | _ => raise ERROR);
    1.12 @@ -127,7 +127,7 @@
    1.13          | term_of [~1] = const "MinusSign"
    1.14          | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
    1.15      in
    1.16 -      term_of (bin_of (sign * (#1 (scan_int digs))))
    1.17 +      term_of (bin_of (sign * (#1 (read_int digs))))
    1.18      end;
    1.19  
    1.20    fun dest_bin tm =
     2.1 --- a/src/HOLCF/domain/extender.ML	Mon Mar 09 16:15:24 1998 +0100
     2.2 +++ b/src/HOLCF/domain/extender.ML	Mon Mar 09 16:16:21 1998 +0100
     2.3 @@ -85,9 +85,9 @@
     2.4      val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
     2.5      val dts  = map (Type o fst) eqs';
     2.6      fun strip ss = drop (find_index_eq "'" ss +1, ss);
     2.7 -    fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
     2.8 -      | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
     2.9 -      | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
    2.10 +    fun typid (Type  (id,_)   ) = hd     (Symbol.explode (Sign.base_name id))
    2.11 +      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode (Sign.base_name id))))
    2.12 +      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode (Sign.base_name id)));
    2.13      fun cons cons' = (map (fn (con,syn,args) =>
    2.14  	((Syntax.const_name con syn),
    2.15  	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
     3.1 --- a/src/HOLCF/domain/interface.ML	Mon Mar 09 16:15:24 1998 +0100
     3.2 +++ b/src/HOLCF/domain/interface.ML	Mon Mar 09 16:16:21 1998 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5    fun get      dname name   = "get_thm thy " ^ quote (dname^"."^name);
     3.6    fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
     3.7 -			(if hd (rev (explode name)) = "s" then "s" else "")^
     3.8 +			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
     3.9  			" thy " ^ quote (dname^"."^name)^";";
    3.10    fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
    3.11    val rews = "iso_rews @ when_rews @\n\
    3.12 @@ -109,7 +109,7 @@
    3.13  			|   esc ("[" ::xs) = "{"::esc xs
    3.14  			|   esc ("]" ::xs) = "}"::esc xs
    3.15  			|   esc (x   ::xs) = x  ::esc xs
    3.16 -		    in implode (esc (explode s)) end;
    3.17 +		    in implode (esc (Symbol.explode s)) end;
    3.18    val tvar = (type_var' ^^ 
    3.19  	      optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
    3.20    fun type_args l = (tvar >> (fn x => [x])
     4.1 --- a/src/HOLCF/domain/library.ML	Mon Mar 09 16:15:24 1998 +0100
     4.2 +++ b/src/HOLCF/domain/library.ML	Mon Mar 09 16:16:21 1998 +0100
     4.3 @@ -50,9 +50,9 @@
     4.4  		    |   strip ["'"] = []
     4.5  		    |   strip (c :: cs) = c :: strip cs
     4.6  		    |   strip [] = [];
     4.7 -in implode o strip o explode end;
     4.8 +in implode o strip o Symbol.explode end;
     4.9  
    4.10 -fun extern_name con = case explode con of 
    4.11 +fun extern_name con = case Symbol.explode con of 
    4.12  		   ("o"::"p"::" "::rest) => implode rest
    4.13  		   | _ => con;
    4.14  fun dis_name  con = "is_"^ (extern_name con);
     5.1 --- a/src/HOLCF/domain/syntax.ML	Mon Mar 09 16:15:24 1998 +0100
     5.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Mar 09 16:16:21 1998 +0100
     5.3 @@ -42,7 +42,7 @@
     5.4  	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
     5.5  							 else      c::esc cs
     5.6  	|   esc []      = []
     5.7 -	in implode o esc o explode end;
     5.8 +	in implode o esc o Symbol.explode end;
     5.9    fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
    5.10    fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
    5.11  			   Mixfix(escape ("is_" ^ con), [], max_pri));
     6.1 --- a/src/ZF/ex/Bin.thy	Mon Mar 09 16:15:24 1998 +0100
     6.2 +++ b/src/ZF/ex/Bin.thy	Mon Mar 09 16:16:21 1998 +0100
     6.3 @@ -117,7 +117,7 @@
     6.4    fun mk_bin str =
     6.5      let
     6.6        val (sign, digs) =
     6.7 -        (case explode str of
     6.8 +        (case Symbol.explode str of
     6.9            "#" :: "~" :: cs => (~1, cs)
    6.10          | "#" :: cs => (1, cs)
    6.11          | _ => raise ERROR);
    6.12 @@ -132,7 +132,7 @@
    6.13          | term_of [~1] = const "Minus"
    6.14          | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
    6.15      in
    6.16 -      term_of (bin_of (sign * (#1 (scan_int digs))))
    6.17 +      term_of (bin_of (sign * (#1 (read_int digs))))
    6.18      end;
    6.19  
    6.20    fun dest_bin tm =