src/HOL/List.thy

       | string_ast_tr asts = raise AST ("string_tr", asts);
   in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
 *}
 
 ML {*
+structure HOList =
+struct
+
+local
+  val thy = the_context ();
+in
+  val typ_string = Type (Sign.intern_type thy "string", []);
+  fun typ_list ty = Type (Sign.intern_type thy "list", [ty]);
+  fun term_list ty f [] = Const (Sign.intern_const thy "Nil", typ_list ty)
+    | term_list ty f (x::xs) = Const (Sign.intern_const thy "Cons",
+        ty --> typ_list ty --> typ_list ty) $ f x $ term_list ty f xs;
+end;
+
 fun int_of_nibble h =
   if "0" <= h andalso h <= "9" then ord h - ord "0"
   else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
   else raise Match;
 
 fun nibble_of_int i =
   if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
 
-fun term_of_string s =
+fun term_string s =
   let
     val ty_n = Type ("List.nibble", []);
     val ty_c = Type ("List.char", []);
     val ty_l = Type ("List.list", [ty_c]);
     fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)), ty_n);

         Const ("List.char.Char", ty_n --> ty_n --> ty_c) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16)
       else error ("Printable ASCII character expected: " ^ quote c);
     fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l)
       $ mk_char c $ t;
   in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end;
+
+end;
 *}
 
 print_ast_translation {*
   let
     fun dest_nib (Syntax.Constant c) =
         (case explode c of
-          ["N", "i", "b", "b", "l", "e", h] => int_of_nibble h
+          ["N", "i", "b", "b", "l", "e", h] => HOList.int_of_nibble h
         | _ => raise Match)
       | dest_nib _ = raise Match;
 
     fun dest_chr c1 c2 =
       let val c = chr (dest_nib c1 * 16 + dest_nib c2)

     (gr, HOLogic.dest_list t)
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
       let
-        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
+        fun dest_nibble (Const (s, _)) = (HOList.int_of_nibble o unprefix "List.nibble.Nibble") s
           | dest_nibble _ = raise Match;
       in
         (SOME (dest_nibble c1 * 16 + dest_nibble c2)
         handle Fail _ => NONE | Match => NONE)
       end

 attach (term_of) {*
 val nibbleT = Type ("List.nibble", []);
 
 fun term_of_char c =
   Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $
-    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c div 16), nibbleT) $
-    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c mod 16), nibbleT);
+    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c div 16), nibbleT) $
+    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c mod 16), nibbleT);
 *}
 attach (test) {*
 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
 *}