# HG changeset patch
# User wenzelm
# Date 979601154 -3600
# Node ID 624077d5afddda4252395747cba7c017d9bbccd6
# Parent  ad1fb17361e49cec62282db8bc951487b4bd8004
removed;

diff -r ad1fb17361e4 -r 624077d5afdd src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Tue Jan 16 00:25:25 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(*  Title:      HOL/Tools/string_syntax.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Concrete syntax for hex chars and strings.  Assumes consts and syntax
-of theory HOL/String.
-*)
-
-signature STRING_SYNTAX =
-sig
-  val setup: (theory -> theory) list
-end;
-
-structure StringSyntax: STRING_SYNTAX =
-struct
-
-
-(* chars *)
-
-fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
-
-
-val zero = ord "0";
-val ten = ord "A" - 10;
-
-fun mk_nib n =
-  Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
-
-fun dest_nib (Const (c, _)) =
-      (case explode c of
-        ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
-      | _ => raise Match)
-  | dest_nib _ = raise Match;
-
-fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
-
-
-fun mk_char c =
-  Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
-
-fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
-  | dest_char _ = raise Match;
-
-
-fun char_tr (*"_Char"*) [Free (xstr, _)] =
-      (case Syntax.explode_xstr xstr of
-        [c] => mk_char c
-      | _ => error ("Single character expected: " ^ xstr))
-  | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
-
-fun char_tr' (*"Char"*) [t1, t2] =
-      Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
-  | char_tr' (*"Char"*) _ = raise Match;
-
-
-(* strings *)
-
-fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
-  | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
-
-fun dest_string (Const ("Nil", _)) = []
-  | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
-  | dest_string _ = raise Match;
-
-
-fun string_tr (*"_String"*) [Free (xstr, _)] =
-      mk_string (map mk_char (Syntax.explode_xstr xstr))
-  | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
-
-fun cons_tr' (*"Cons"*) [c, cs] =
-      Syntax.const "_String" $
-        syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
-  | cons_tr' (*"Cons"*) ts = raise Match;
-
-
-(* theory setup *)
-
-val setup =
-  [Theory.add_trfuns
-    ([], [("_Char", char_tr), ("_String", string_tr)],
-    [("Char", char_tr'), ("Cons", cons_tr')], [])];
-
-end;