src/HOLCF/domain/syntax.ML
changeset 4709 d24168720303
parent 4122 f63c283cefaf
child 5291 5706f0ef1d43
     1.1 --- a/src/HOLCF/domain/syntax.ML	Mon Mar 09 16:15:24 1998 +0100
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Mar 09 16:16:21 1998 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
     1.5  							 else      c::esc cs
     1.6  	|   esc []      = []
     1.7 -	in implode o esc o explode end;
     1.8 +	in implode o esc o Symbol.explode end;
     1.9    fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
    1.10    fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
    1.11  			   Mixfix(escape ("is_" ^ con), [], max_pri));