diff --git a/Nano_JSON.thy b/Nano_JSON.thy
index 60d7af9..75a87ef 100644
--- a/Nano_JSON.thy
+++ b/Nano_JSON.thy
@@ -159,10 +159,78 @@ end
 
 section\<open>Serializing Nano JSON\<close>
 
+ML\<open>
+signature NANO_JSON_SERIALIZER = sig
+    val serialize_json: Nano_Json_Type.json -> string
+    val serialize_json_pretty: Nano_Json_Type.json -> string
+    val serialize_term: term -> string
+    val serialize_term_pretty: term -> string
+end
+
+structure Nano_Json_Serializer : NANO_JSON_SERIALIZER = struct
+    open Nano_Json_Type
+    fun escapeJsonString s =
+        let fun bs c = "\\"^(Char.toString c)
+            fun escape #"\"" = bs #"\"" 
+              | escape #"\\" = bs #"\\" 
+              | escape #"\b" = bs #"b"
+              | escape #"\f" = bs #"f"
+              | escape #"\n" = bs #"n"
+              | escape #"\r" = bs #"r"
+              | escape #"\t" = bs #"t"
+              | escape c = 
+                let val ord = Char.ord c
+                in
+                    if ord < 0x20
+                    then let val hex = Word.toString (Word.fromInt ord)
+                             val prfx = if ord < 0x10 then "\\u000" else "\\u00"
+                         in  
+                             prfx^hex
+                         end
+                    else
+                    Char.toString c
+                end
+        in
+            String.concat (map escape (String.explode s))
+        end
+
+    fun serialize pretty json = let 
+            val nl = if pretty = NONE then "" else "\n"
+            fun indent' 0 = ""
+              | indent' n = " "^(indent' (n-1)) 
+            fun indent n = (case pretty of NONE => "" 
+                                         | SOME n' => indent' (n+n'))
+            fun serialize' _ (OBJECT []) = "{}"
+              | serialize' _ (ARRAY []) = "[]"
+              | serialize' n (OBJECT pp) = "{"^nl^(indent (n+1)) ^ String.concatWith
+                                   (","^nl^(indent (n+1))) 
+                                   (map (fn (key, value) =>
+                                                serialize' (n+1) (STRING key) ^ ":" ^
+                                                serialize' (n+1) value) pp) ^
+                                   nl^(indent n)^"}"
+              | serialize' n (ARRAY arr) = "["^nl^(indent (n+1)) ^ String.concatWith
+                                           (","^nl^(indent (n+1)))
+                                           (map (serialize' (n+1) ) arr) ^
+                                   nl^(indent n)^"]"
+              | serialize' _ (NUMBER (REAL n)) = String.implode (map (fn #"~" => #"-" | c => c)
+                                     (String.explode (Real.toString n)))
+              | serialize' _ (NUMBER (INTEGER n)) = String.implode (map (fn #"~" => #"-" | c => c)
+                                     (String.explode (Int.toString n)))
+              | serialize' _ (STRING s) = "\"" ^ escapeJsonString s ^ "\""
+              | serialize' _ (BOOL b) = Bool.toString b
+              | serialize' _ NULL = "null"
+            
+        in
+            (serialize' 0 json)^nl
+        end
+
+    val serialize_json = serialize NONE
+    val serialize_json_pretty = serialize (SOME 0)
+    val serialize_term = (serialize NONE) o json_of_term
+    val serialize_term_pretty = (serialize (SOME 0)) o json_of_term
+end
+\<close>
 
 section\<open>Parsing Nano JSON\<close>
 
-
-
-
 end