src/HOL/Tools/string_syntax.ML

 
 
 (* nibble *)
 
 val mk_nib =
-  Syntax.Constant o Syntax.mark_const o
+  Ast.Constant o Syntax.mark_const o
     fst o Term.dest_Const o HOLogic.mk_nibble;
 
-fun dest_nib (Syntax.Constant s) =
+fun dest_nib (Ast.Constant s) =
   (case try Syntax.unmark_const s of
     NONE => raise Match
   | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
 
 
 (* char *)
 
 fun mk_char s =
   if Symbol.is_ascii s then
-    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
+    Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
   else error ("Non-ASCII symbol: " ^ quote s);
 
 val specials = raw_explode "\\\"`'";
 
 fun dest_chr c1 c2 =
   let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
     if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
     then c else raise Match
   end;
 
-fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
+fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   | dest_char _ = raise Match;
 
 fun syntax_string cs =
-  Syntax.Appl
-    [Syntax.Constant @{syntax_const "_inner_string"},
-      Syntax.Variable (Syntax.implode_xstr cs)];
+  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
 
 
-fun char_ast_tr [Syntax.Variable xstr] =
-    (case Syntax.explode_xstr xstr of
-      [c] => mk_char c
-    | _ => error ("Single character expected: " ^ xstr))
-  | char_ast_tr asts = raise AST ("char_ast_tr", asts);
+fun char_ast_tr [Ast.Variable xstr] =
+      (case Syntax.explode_xstr xstr of
+        [c] => mk_char c
+      | _ => error ("Single character expected: " ^ xstr))
+  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
 
 fun char_ast_tr' [c1, c2] =
-      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
+      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
   | char_ast_tr' _ = raise Match;
 
 
 (* string *)
 
-fun mk_string [] = Syntax.Constant @{const_syntax Nil}
+fun mk_string [] = Ast.Constant @{const_syntax Nil}
   | mk_string (c :: cs) =
-      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
+      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
 
-fun string_ast_tr [Syntax.Variable xstr] =
-    (case Syntax.explode_xstr xstr of
-      [] =>
-        Syntax.Appl
-          [Syntax.Constant Syntax.constrainC,
-            Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
-    | cs => mk_string cs)
-  | string_ast_tr asts = raise AST ("string_tr", asts);
+fun string_ast_tr [Ast.Variable xstr] =
+      (case Syntax.explode_xstr xstr of
+        [] =>
+          Ast.Appl
+            [Ast.Constant Syntax.constrainC,
+              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
+      | cs => mk_string cs)
+  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
 
 fun list_ast_tr' [args] =
-      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
-        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
+      Ast.Appl [Ast.Constant @{syntax_const "_String"},
+        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
   | list_ast_tr' ts = raise Match;
 
 
 (* theory setup *)