qualified String.explode and String.implode

--- a/NEWS	Sun Jun 29 21:07:53 2014 +0200
+++ b/NEWS	Mon Jun 30 08:00:36 2014 +0200
@@ -178,6 +178,8 @@
 
 *** HOL ***
 
+* Qualified String.implode and String.explode.  INCOMPATIBILITY.
+
 * Command and antiquotation ''value'' are hardcoded against nbe and
 ML now.  Minor INCOMPATIBILITY.
 

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Jun 29 21:07:53 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 30 08:00:36 2014 +0200
@@ -546,7 +546,7 @@
 subsubsection {* Logical intermediate layer *}
 
 definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
-  [code del]: "raise' s = raise (explode s)"
+  [code del]: "raise' s = raise (String.explode s)"
 
 lemma [code_abbrev]: "raise' (STR s) = raise s"
   unfolding raise'_def by (simp add: STR_inverse)

--- a/src/HOL/Library/Char_ord.thy	Sun Jun 29 21:07:53 2014 +0200
+++ b/src/HOL/Library/Char_ord.thy	Mon Jun 30 08:00:36 2014 +0200
@@ -113,11 +113,11 @@
 end
 
 lemma less_literal_code [code]: 
-  "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
+  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
 by(simp add: less_literal.rep_eq fun_eq_iff)
 
 lemma less_eq_literal_code [code]:
-  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
+  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
 by(simp add: less_eq_literal.rep_eq fun_eq_iff)
 
 lifting_update literal.lifting

--- a/src/HOL/Library/Code_Char.thy	Sun Jun 29 21:07:53 2014 +0200
+++ b/src/HOL/Library/Code_Char.thy	Mon Jun 30 08:00:36 2014 +0200
@@ -40,18 +40,15 @@
 code_reserved Scala
   char
 
-definition implode :: "string \<Rightarrow> String.literal" where
-  "implode = STR"
-
 code_reserved SML String
 
 code_printing
-  constant implode \<rightharpoonup>
+  constant String.implode \<rightharpoonup>
     (SML) "String.implode"
     and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)"
     and (Haskell) "_"
     and (Scala) "!(\"\" ++/ _)"
-| constant explode \<rightharpoonup>
+| constant String.explode \<rightharpoonup>
     (SML) "String.explode"
     and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])"
     and (Haskell) "_"

--- a/src/HOL/Library/Countable.thy	Sun Jun 29 21:07:53 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Mon Jun 30 08:00:36 2014 +0200
@@ -104,7 +104,7 @@
 text {* Further *}
 
 instance String.literal :: countable
-  by (rule countable_classI [of "to_nat o explode"])
+  by (rule countable_classI [of "to_nat o String.explode"])
     (auto simp add: explode_inject)
 
 text {* Functions *}

--- a/src/HOL/String.thy	Sun Jun 29 21:07:53 2014 +0200
+++ b/src/HOL/String.thy	Mon Jun 30 08:00:36 2014 +0200
@@ -358,6 +358,10 @@
 
 setup_lifting (no_code) type_definition_literal
 
+definition implode :: "string \<Rightarrow> String.literal"
+where
+  "implode = STR"
+
 instantiation literal :: size
 begin
 
@@ -440,4 +444,6 @@
 
 hide_type (open) literal
 
+hide_const (open) implode explode
+
 end