# HG changeset patch
# User wenzelm
# Date 1302006318 -7200
# Node ID 578a51fae383be3f86cea0d6d29e09a01af28604
# Parent  098c86e53153ab84b2fb6ba538b0d23e9befbc39
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

diff -r 098c86e53153 -r 578a51fae383 NEWS
--- a/NEWS	Tue Apr 05 13:07:40 2011 +0200
+++ b/NEWS	Tue Apr 05 14:25:18 2011 +0200
@@ -93,6 +93,10 @@
 be disabled via the configuration option Syntax.positions, which is
 called "syntax_positions" in Isar attribute syntax.
 
+* Discontinued special treatment of structure Ast: no pervasive
+content, no inclusion in structure Syntax.  INCOMPATIBILITY, refer to
+qualified names like Ast.Constant etc.
+
 
 
 New in Isabelle2011 (January 2011)
diff -r 098c86e53153 -r 578a51fae383 doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Tue Apr 05 13:07:40 2011 +0200
+++ b/doc-src/Classes/Thy/Setup.thy	Tue Apr 05 14:25:18 2011 +0200
@@ -15,16 +15,16 @@
 
 parse_ast_translation {*
   let
-    fun alpha_ast_tr [] = Syntax.Variable "'a"
-      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+    fun alpha_ast_tr [] = Ast.Variable "'a"
+      | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
     fun alpha_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
-      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
-    fun beta_ast_tr [] = Syntax.Variable "'b"
-      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
+      | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
+    fun beta_ast_tr [] = Ast.Variable "'b"
+      | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
     fun beta_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
-      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
+      | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
   in
    [(@{syntax_const "_alpha"}, alpha_ast_tr),
     (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
diff -r 098c86e53153 -r 578a51fae383 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 14:25:18 2011 +0200
@@ -56,9 +56,9 @@
 (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
   let
     fun Lambda_ast_tr [pats, body] =
-          Syntax.fold_ast_p @{syntax_const "_cabs"}
-            (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
-      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
+          Ast.fold_ast_p @{syntax_const "_cabs"}
+            (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
+      | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
   in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
 *}
 
@@ -67,12 +67,12 @@
 (* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
   let
     fun cabs_ast_tr' asts =
-      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
-          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
-        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
-      | (xs, body) => Syntax.Appl
-          [Syntax.Constant @{syntax_const "_Lambda"},
-           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
+      (case Ast.unfold_ast_p @{syntax_const "_cabs"}
+          (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of
+        ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
+      | (xs, body) => Ast.Appl
+          [Ast.Constant @{syntax_const "_Lambda"},
+           Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
   in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
 *}
 
diff -r 098c86e53153 -r 578a51fae383 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -442,16 +442,14 @@
     (* define syntax for case combinator *)
     (* TODO: re-implement case syntax using a parse translation *)
     local
-      open Syntax
       fun syntax c = Syntax.mark_const (fst (dest_Const c))
       fun xconst c = Long_Name.base_name (fst (dest_Const c))
-      fun c_ast authentic con =
-          Constant (if authentic then syntax con else xconst con)
+      fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
       fun showint n = string_of_int (n+1)
-      fun expvar n = Variable ("e" ^ showint n)
-      fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m)
+      fun expvar n = Ast.Variable ("e" ^ showint n)
+      fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m)
       fun argvars n args = map_index (argvar n) args
-      fun app s (l, r) = mk_appl (Constant s) [l, r]
+      fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]
       val cabs = app "_cabs"
       val capp = app @{const_syntax Rep_cfun}
       val capps = Library.foldl capp
@@ -460,22 +458,21 @@
       fun case1 authentic (n, c) =
           app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
       fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
-      fun when1 n (m, c) =
-          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
-      val case_constant = Constant (syntax (case_const dummyT))
+      fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
+      val case_constant = Ast.Constant (syntax (case_const dummyT))
       fun case_trans authentic =
-          (if authentic then Parse_Print_Rule else Parse_Rule)
-            (app "_case_syntax"
-              (Variable "x",
-               foldr1 (app "_case2") (map_index (case1 authentic) spec)),
-             capp (capps (case_constant, map_index arg1 spec), Variable "x"))
+        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+          (app "_case_syntax"
+            (Ast.Variable "x",
+             foldr1 (app "_case2") (map_index (case1 authentic) spec)),
+           capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
       fun one_abscon_trans authentic (n, c) =
-          (if authentic then Parse_Print_Rule else Parse_Rule)
-            (cabs (con1 authentic n c, expvar n),
-             capps (case_constant, map_index (when1 n) spec))
+        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+          (cabs (con1 authentic n c, expvar n),
+           capps (case_constant, map_index (when1 n) spec))
       fun abscon_trans authentic =
           map_index (one_abscon_trans authentic) spec
-      val trans_rules : ast Syntax.trrule list =
+      val trans_rules : Ast.ast Syntax.trrule list =
           case_trans false :: case_trans true ::
           abscon_trans false @ abscon_trans true
     in
diff -r 098c86e53153 -r 578a51fae383 src/HOL/HOLCF/Tools/cont_consts.ML
--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -24,12 +24,13 @@
 fun trans_rules name2 name1 n mx =
   let
     val vnames = Name.invents Name.context "a" n
-    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
+    val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
   in
     [Syntax.Parse_Print_Rule
-      (Syntax.mk_appl (Constant name2) (map Variable vnames),
-        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
-          vnames (Constant name1))] @
+      (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
+        fold (fn a => fn t =>
+            Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a])
+          vnames (Ast.Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]
     | Infixl _ => [extra_parse_rule]
diff -r 098c86e53153 -r 578a51fae383 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Apr 05 14:25:18 2011 +0200
@@ -497,33 +497,32 @@
 
     (* syntax translations for pattern combinators *)
     local
-      open Syntax
       fun syntax c = Syntax.mark_const (fst (dest_Const c));
-      fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
+      fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
       val capp = app @{const_syntax Rep_cfun};
       val capps = Library.foldl capp
 
-      fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
-      fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
-      fun args_list [] = Constant "_noargs"
+      fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"];
+      fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x];
+      fun args_list [] = Ast.Constant "_noargs"
         | args_list xs = foldr1 (app "_args") xs;
       fun one_case_trans (pat, (con, args)) =
         let
-          val cname = Constant (syntax con);
-          val pname = Constant (syntax pat);
+          val cname = Ast.Constant (syntax con);
+          val pname = Ast.Constant (syntax pat);
           val ns = 1 upto length args;
-          val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
-          val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
-          val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
+          val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns;
+          val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns;
+          val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns;
         in
-          [Parse_Rule (app_pat (capps (cname, xs)),
-                      mk_appl pname (map app_pat xs)),
-           Parse_Rule (app_var (capps (cname, xs)),
-                      app_var (args_list xs)),
-           Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
-                      app "_match" (mk_appl pname ps, args_list vs))]
+          [Syntax.Parse_Rule (app_pat (capps (cname, xs)),
+            Ast.mk_appl pname (map app_pat xs)),
+           Syntax.Parse_Rule (app_var (capps (cname, xs)),
+            app_var (args_list xs)),
+           Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
+            app "_match" (Ast.mk_appl pname ps, args_list vs))]
         end;
-      val trans_rules : Syntax.ast Syntax.trrule list =
+      val trans_rules : Ast.ast Syntax.trrule list =
           maps one_case_trans (pat_consts ~~ spec);
     in
       val thy = Sign.add_trrules trans_rules thy;
diff -r 098c86e53153 -r 578a51fae383 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -610,10 +610,10 @@
     end
 
 local
-    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
-      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
-      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
-      | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
+    fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x
+      | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x
+      | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x
+      | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x]
       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
 in
 val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
diff -r 098c86e53153 -r 578a51fae383 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/Tools/string_syntax.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -16,10 +16,10 @@
 (* 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));
@@ -29,7 +29,7 @@
 
 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 "\\\"`'";
@@ -40,44 +40,42 @@
     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;
 
 
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -398,8 +398,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.ast_trace_raw #>
-  register_config Syntax.ast_stat_raw #>
+ (register_config Ast.ast_trace_raw #>
+  register_config Ast.ast_stat_raw #>
   register_config Syntax.positions_raw #>
   register_config Syntax.show_brackets_raw #>
   register_config Syntax.show_sorts_raw #>
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -117,7 +117,7 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     ("val parse_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
+      "Ast.ast list -> Ast.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   |> Context.theory_map;
 
@@ -141,7 +141,7 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     ("val print_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
+      "Ast.ast list -> Ast.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   |> Context.theory_map;
 
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -1093,12 +1093,12 @@
 
 local
 
-fun const_ast_tr intern ctxt [Syntax.Variable c] =
+fun const_ast_tr intern ctxt [Ast.Variable c] =
       let
         val Const (c', _) = read_const_proper ctxt false c;
         val d = if intern then Syntax.mark_const c' else c;
-      in Syntax.Constant d end
-  | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+      in Ast.Constant d end
+  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
 
 val typ = Simple_Syntax.read_typ;
 
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -72,9 +72,9 @@
         | Fail msg => [raised exn "Fail" [msg]]
         | THEORY (msg, thys) =>
             [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
-        | Syntax.AST (msg, asts) =>
+        | Ast.AST (msg, asts) =>
             [raised exn "AST" (msg ::
-              (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
         | TYPE (msg, Ts, ts) =>
             [raised exn "TYPE" (msg ::
               (if detailed then
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -71,17 +71,20 @@
   |> Sign.add_modesyntax_i ("latex", false)
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
   |> Sign.add_trrules (map Syntax.Parse_Print_Rule
-      [(Syntax.mk_appl (Constant "_Lam")
-          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
-        Syntax.mk_appl (Constant "_Lam")
-          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
-       (Syntax.mk_appl (Constant "_Lam")
-          [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
-        Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
-          (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
-       (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
-        Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
-          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
+      [(Ast.mk_appl (Ast.Constant "_Lam")
+          [Ast.mk_appl (Ast.Constant "_Lam0")
+            [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
+        Ast.mk_appl (Ast.Constant "_Lam")
+          [Ast.Variable "l",
+            Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
+       (Ast.mk_appl (Ast.Constant "_Lam")
+          [Ast.mk_appl (Ast.Constant "_Lam1")
+            [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
+        Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
+          (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
+       (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
+        Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
+          [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
 
 
 (**** translation between proof terms and pure terms ****)
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -4,21 +4,18 @@
 Abstract syntax trees, translation rules, matching and normalization of asts.
 *)
 
-signature AST0 =
+signature AST =
 sig
   datatype ast =
     Constant of string |
     Variable of string |
     Appl of ast list
+  val mk_appl: ast -> ast list -> ast
   exception AST of string * ast list
-end;
-
-signature AST1 =
-sig
-  include AST0
-  val mk_appl: ast -> ast list -> ast
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
+  val head_of_rule: ast * ast -> string
+  val rule_error: ast * ast -> string option
   val fold_ast: string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
@@ -27,17 +24,10 @@
   val ast_trace: bool Config.T
   val ast_stat_raw: Config.raw
   val ast_stat: bool Config.T
-end;
-
-signature AST =
-sig
-  include AST1
-  val head_of_rule: ast * ast -> string
-  val rule_error: ast * ast -> string option
   val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
 
-structure Ast : AST =
+structure Ast: AST =
 struct
 
 (** abstract syntax trees **)
@@ -53,16 +43,12 @@
   Variable of string |    (*x, ?x, 'a, ?'a*)
   Appl of ast list;       (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
 
-
 (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
   there are no empty asts or nullary applications; use mk_appl for convenience*)
-
 fun mk_appl f [] = f
   | mk_appl f args = Appl (f :: args);
 
-
 (*exception for system errors involving asts*)
-
 exception AST of string * ast list;
 
 
diff -r 098c86e53153 -r 578a51fae383 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_SYNTAX =
 sig
-  include AST0
   include SYN_TRANS0
   include MIXFIX0
   include PRINTER0
@@ -15,7 +14,6 @@
 
 signature SYNTAX =
 sig
-  include AST1
   include LEXICON0
   include SYN_EXT0
   include TYPE_EXT0
@@ -129,7 +127,7 @@
     Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val is_const: syntax -> string -> bool
-  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
+  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> Ast.ast
   val standard_unparse_sort: {extern_class: string -> xstring} ->
     Proof.context -> syntax -> sort -> Pretty.T
   val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
@@ -138,22 +136,22 @@
     {extern_class: string -> xstring, extern_type: string -> xstring,
       extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   val update_trfuns:
-    (string * ((ast list -> ast) * stamp)) list *
+    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
+    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val update_advanced_trfuns:
-    (string * ((Proof.context -> ast list -> ast) * stamp)) list *
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
     syntax -> syntax
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_trrules: ast trrule list -> syntax -> syntax
-  val remove_trrules: ast trrule list -> syntax -> syntax
+  val update_trrules: Ast.ast trrule list -> syntax -> syntax
+  val remove_trrules: Ast.ast trrule list -> syntax -> syntax
 end;
 
 structure Syntax: SYNTAX =
@@ -943,14 +941,13 @@
 
 
 (*export parts of internal Syntax structures*)
-open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Parser Type_Ext Syn_Trans Mixfix Printer;
 
 end;
 
 structure Basic_Syntax: BASIC_SYNTAX = Syntax;
 open Basic_Syntax;
 
-forget_structure "Ast";
 forget_structure "Syn_Ext";
 forget_structure "Parser";
 forget_structure "Type_Ext";
diff -r 098c86e53153 -r 578a51fae383 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/pure_setup.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -30,7 +30,7 @@
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
-toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Syntax", "ast"] "Ast.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
diff -r 098c86e53153 -r 578a51fae383 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/sign.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -91,25 +91,25 @@
   val primitive_classrel: class * class -> theory -> theory
   val primitive_arity: arity -> theory -> theory
   val add_trfuns:
-    (string * (ast list -> ast)) list *
+    (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
-    (string * (ast list -> ast)) list -> theory -> theory
+    (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_trfunsT:
     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   val add_advanced_trfuns:
-    (string * (Proof.context -> ast list -> ast)) list *
+    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
     (string * (Proof.context -> term list -> term)) list *
     (string * (Proof.context -> term list -> term)) list *
-    (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
+    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_advanced_trfunsT:
     (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
     (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
     -> theory -> theory
-  val add_trrules: ast Syntax.trrule list -> theory -> theory
-  val del_trrules: ast Syntax.trrule list -> theory -> theory
+  val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+  val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   val new_group: theory -> theory
   val reset_group: theory -> theory
   val add_path: string -> theory -> theory