1.1 --- a/NEWS	Tue Apr 05 13:07:40 2011 +0200
     1.2 +++ b/NEWS	Tue Apr 05 14:25:18 2011 +0200
     1.3 @@ -93,6 +93,10 @@
     1.4  be disabled via the configuration option Syntax.positions, which is
     1.5  called "syntax_positions" in Isar attribute syntax.
     1.6  
     1.7 +* Discontinued special treatment of structure Ast: no pervasive
     1.8 +content, no inclusion in structure Syntax.  INCOMPATIBILITY, refer to
     1.9 +qualified names like Ast.Constant etc.
    1.10 +
    1.11  
    1.12  
    1.13  New in Isabelle2011 (January 2011)

     2.1 --- a/doc-src/Classes/Thy/Setup.thy	Tue Apr 05 13:07:40 2011 +0200
     2.2 +++ b/doc-src/Classes/Thy/Setup.thy	Tue Apr 05 14:25:18 2011 +0200
     2.3 @@ -15,16 +15,16 @@
     2.4  
     2.5  parse_ast_translation {*
     2.6    let
     2.7 -    fun alpha_ast_tr [] = Syntax.Variable "'a"
     2.8 -      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
     2.9 +    fun alpha_ast_tr [] = Ast.Variable "'a"
    2.10 +      | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
    2.11      fun alpha_ofsort_ast_tr [ast] =
    2.12 -      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
    2.13 -      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    2.14 -    fun beta_ast_tr [] = Syntax.Variable "'b"
    2.15 -      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    2.16 +          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
    2.17 +      | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
    2.18 +    fun beta_ast_tr [] = Ast.Variable "'b"
    2.19 +      | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
    2.20      fun beta_ofsort_ast_tr [ast] =
    2.21 -      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
    2.22 -      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    2.23 +          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
    2.24 +      | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
    2.25    in
    2.26     [(@{syntax_const "_alpha"}, alpha_ast_tr),
    2.27      (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),

     3.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 13:07:40 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 14:25:18 2011 +0200
     3.3 @@ -56,9 +56,9 @@
     3.4  (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
     3.5    let
     3.6      fun Lambda_ast_tr [pats, body] =
     3.7 -          Syntax.fold_ast_p @{syntax_const "_cabs"}
     3.8 -            (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
     3.9 -      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    3.10 +          Ast.fold_ast_p @{syntax_const "_cabs"}
    3.11 +            (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
    3.12 +      | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
    3.13    in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
    3.14  *}
    3.15  
    3.16 @@ -67,12 +67,12 @@
    3.17  (* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
    3.18    let
    3.19      fun cabs_ast_tr' asts =
    3.20 -      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
    3.21 -          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
    3.22 -        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
    3.23 -      | (xs, body) => Syntax.Appl
    3.24 -          [Syntax.Constant @{syntax_const "_Lambda"},
    3.25 -           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
    3.26 +      (case Ast.unfold_ast_p @{syntax_const "_cabs"}
    3.27 +          (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of
    3.28 +        ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
    3.29 +      | (xs, body) => Ast.Appl
    3.30 +          [Ast.Constant @{syntax_const "_Lambda"},
    3.31 +           Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
    3.32    in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
    3.33  *}
    3.34  

     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 13:07:40 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 14:25:18 2011 +0200
     4.3 @@ -442,16 +442,14 @@
     4.4      (* define syntax for case combinator *)
     4.5      (* TODO: re-implement case syntax using a parse translation *)
     4.6      local
     4.7 -      open Syntax
     4.8        fun syntax c = Syntax.mark_const (fst (dest_Const c))
     4.9        fun xconst c = Long_Name.base_name (fst (dest_Const c))
    4.10 -      fun c_ast authentic con =
    4.11 -          Constant (if authentic then syntax con else xconst con)
    4.12 +      fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
    4.13        fun showint n = string_of_int (n+1)
    4.14 -      fun expvar n = Variable ("e" ^ showint n)
    4.15 -      fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m)
    4.16 +      fun expvar n = Ast.Variable ("e" ^ showint n)
    4.17 +      fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m)
    4.18        fun argvars n args = map_index (argvar n) args
    4.19 -      fun app s (l, r) = mk_appl (Constant s) [l, r]
    4.20 +      fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]
    4.21        val cabs = app "_cabs"
    4.22        val capp = app @{const_syntax Rep_cfun}
    4.23        val capps = Library.foldl capp
    4.24 @@ -460,22 +458,21 @@
    4.25        fun case1 authentic (n, c) =
    4.26            app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
    4.27        fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
    4.28 -      fun when1 n (m, c) =
    4.29 -          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
    4.30 -      val case_constant = Constant (syntax (case_const dummyT))
    4.31 +      fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
    4.32 +      val case_constant = Ast.Constant (syntax (case_const dummyT))
    4.33        fun case_trans authentic =
    4.34 -          (if authentic then Parse_Print_Rule else Parse_Rule)
    4.35 -            (app "_case_syntax"
    4.36 -              (Variable "x",
    4.37 -               foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    4.38 -             capp (capps (case_constant, map_index arg1 spec), Variable "x"))
    4.39 +        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    4.40 +          (app "_case_syntax"
    4.41 +            (Ast.Variable "x",
    4.42 +             foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    4.43 +           capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
    4.44        fun one_abscon_trans authentic (n, c) =
    4.45 -          (if authentic then Parse_Print_Rule else Parse_Rule)
    4.46 -            (cabs (con1 authentic n c, expvar n),
    4.47 -             capps (case_constant, map_index (when1 n) spec))
    4.48 +        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    4.49 +          (cabs (con1 authentic n c, expvar n),
    4.50 +           capps (case_constant, map_index (when1 n) spec))
    4.51        fun abscon_trans authentic =
    4.52            map_index (one_abscon_trans authentic) spec
    4.53 -      val trans_rules : ast Syntax.trrule list =
    4.54 +      val trans_rules : Ast.ast Syntax.trrule list =
    4.55            case_trans false :: case_trans true ::
    4.56            abscon_trans false @ abscon_trans true
    4.57      in

     5.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Apr 05 13:07:40 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Apr 05 14:25:18 2011 +0200
     5.3 @@ -24,12 +24,13 @@
     5.4  fun trans_rules name2 name1 n mx =
     5.5    let
     5.6      val vnames = Name.invents Name.context "a" n
     5.7 -    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
     5.8 +    val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
     5.9    in
    5.10      [Syntax.Parse_Print_Rule
    5.11 -      (Syntax.mk_appl (Constant name2) (map Variable vnames),
    5.12 -        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
    5.13 -          vnames (Constant name1))] @
    5.14 +      (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
    5.15 +        fold (fn a => fn t =>
    5.16 +            Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a])
    5.17 +          vnames (Ast.Constant name1))] @
    5.18      (case mx of
    5.19        Infix _ => [extra_parse_rule]
    5.20      | Infixl _ => [extra_parse_rule]

     6.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Apr 05 13:07:40 2011 +0200
     6.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Apr 05 14:25:18 2011 +0200
     6.3 @@ -497,33 +497,32 @@
     6.4  
     6.5      (* syntax translations for pattern combinators *)
     6.6      local
     6.7 -      open Syntax
     6.8        fun syntax c = Syntax.mark_const (fst (dest_Const c));
     6.9 -      fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
    6.10 +      fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
    6.11        val capp = app @{const_syntax Rep_cfun};
    6.12        val capps = Library.foldl capp
    6.13  
    6.14 -      fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
    6.15 -      fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
    6.16 -      fun args_list [] = Constant "_noargs"
    6.17 +      fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"];
    6.18 +      fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x];
    6.19 +      fun args_list [] = Ast.Constant "_noargs"
    6.20          | args_list xs = foldr1 (app "_args") xs;
    6.21        fun one_case_trans (pat, (con, args)) =
    6.22          let
    6.23 -          val cname = Constant (syntax con);
    6.24 -          val pname = Constant (syntax pat);
    6.25 +          val cname = Ast.Constant (syntax con);
    6.26 +          val pname = Ast.Constant (syntax pat);
    6.27            val ns = 1 upto length args;
    6.28 -          val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
    6.29 -          val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
    6.30 -          val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
    6.31 +          val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns;
    6.32 +          val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns;
    6.33 +          val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns;
    6.34          in
    6.35 -          [Parse_Rule (app_pat (capps (cname, xs)),
    6.36 -                      mk_appl pname (map app_pat xs)),
    6.37 -           Parse_Rule (app_var (capps (cname, xs)),
    6.38 -                      app_var (args_list xs)),
    6.39 -           Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    6.40 -                      app "_match" (mk_appl pname ps, args_list vs))]
    6.41 +          [Syntax.Parse_Rule (app_pat (capps (cname, xs)),
    6.42 +            Ast.mk_appl pname (map app_pat xs)),
    6.43 +           Syntax.Parse_Rule (app_var (capps (cname, xs)),
    6.44 +            app_var (args_list xs)),
    6.45 +           Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    6.46 +            app "_match" (Ast.mk_appl pname ps, args_list vs))]
    6.47          end;
    6.48 -      val trans_rules : Syntax.ast Syntax.trrule list =
    6.49 +      val trans_rules : Ast.ast Syntax.trrule list =
    6.50            maps one_case_trans (pat_consts ~~ spec);
    6.51      in
    6.52        val thy = Sign.add_trrules trans_rules thy;

     7.1 --- a/src/HOL/Import/hol4rews.ML	Tue Apr 05 13:07:40 2011 +0200
     7.2 +++ b/src/HOL/Import/hol4rews.ML	Tue Apr 05 14:25:18 2011 +0200
     7.3 @@ -610,10 +610,10 @@
     7.4      end
     7.5  
     7.6  local
     7.7 -    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
     7.8 -      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
     7.9 -      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
    7.10 -      | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
    7.11 +    fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x
    7.12 +      | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x
    7.13 +      | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x
    7.14 +      | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x]
    7.15        | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
    7.16  in
    7.17  val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]

     8.1 --- a/src/HOL/Tools/string_syntax.ML	Tue Apr 05 13:07:40 2011 +0200
     8.2 +++ b/src/HOL/Tools/string_syntax.ML	Tue Apr 05 14:25:18 2011 +0200
     8.3 @@ -16,10 +16,10 @@
     8.4  (* nibble *)
     8.5  
     8.6  val mk_nib =
     8.7 -  Syntax.Constant o Syntax.mark_const o
     8.8 +  Ast.Constant o Syntax.mark_const o
     8.9      fst o Term.dest_Const o HOLogic.mk_nibble;
    8.10  
    8.11 -fun dest_nib (Syntax.Constant s) =
    8.12 +fun dest_nib (Ast.Constant s) =
    8.13    (case try Syntax.unmark_const s of
    8.14      NONE => raise Match
    8.15    | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
    8.16 @@ -29,7 +29,7 @@
    8.17  
    8.18  fun mk_char s =
    8.19    if Symbol.is_ascii s then
    8.20 -    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    8.21 +    Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    8.22    else error ("Non-ASCII symbol: " ^ quote s);
    8.23  
    8.24  val specials = raw_explode "\\\"`'";
    8.25 @@ -40,44 +40,42 @@
    8.26      then c else raise Match
    8.27    end;
    8.28  
    8.29 -fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
    8.30 +fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
    8.31    | dest_char _ = raise Match;
    8.32  
    8.33  fun syntax_string cs =
    8.34 -  Syntax.Appl
    8.35 -    [Syntax.Constant @{syntax_const "_inner_string"},
    8.36 -      Syntax.Variable (Syntax.implode_xstr cs)];
    8.37 +  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
    8.38  
    8.39  
    8.40 -fun char_ast_tr [Syntax.Variable xstr] =
    8.41 -    (case Syntax.explode_xstr xstr of
    8.42 -      [c] => mk_char c
    8.43 -    | _ => error ("Single character expected: " ^ xstr))
    8.44 -  | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    8.45 +fun char_ast_tr [Ast.Variable xstr] =
    8.46 +      (case Syntax.explode_xstr xstr of
    8.47 +        [c] => mk_char c
    8.48 +      | _ => error ("Single character expected: " ^ xstr))
    8.49 +  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
    8.50  
    8.51  fun char_ast_tr' [c1, c2] =
    8.52 -      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
    8.53 +      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
    8.54    | char_ast_tr' _ = raise Match;
    8.55  
    8.56  
    8.57  (* string *)
    8.58  
    8.59 -fun mk_string [] = Syntax.Constant @{const_syntax Nil}
    8.60 +fun mk_string [] = Ast.Constant @{const_syntax Nil}
    8.61    | mk_string (c :: cs) =
    8.62 -      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
    8.63 +      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
    8.64  
    8.65 -fun string_ast_tr [Syntax.Variable xstr] =
    8.66 -    (case Syntax.explode_xstr xstr of
    8.67 -      [] =>
    8.68 -        Syntax.Appl
    8.69 -          [Syntax.Constant Syntax.constrainC,
    8.70 -            Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
    8.71 -    | cs => mk_string cs)
    8.72 -  | string_ast_tr asts = raise AST ("string_tr", asts);
    8.73 +fun string_ast_tr [Ast.Variable xstr] =
    8.74 +      (case Syntax.explode_xstr xstr of
    8.75 +        [] =>
    8.76 +          Ast.Appl
    8.77 +            [Ast.Constant Syntax.constrainC,
    8.78 +              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
    8.79 +      | cs => mk_string cs)
    8.80 +  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
    8.81  
    8.82  fun list_ast_tr' [args] =
    8.83 -      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
    8.84 -        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
    8.85 +      Ast.Appl [Ast.Constant @{syntax_const "_String"},
    8.86 +        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
    8.87    | list_ast_tr' ts = raise Match;
    8.88  
    8.89  

     9.1 --- a/src/Pure/Isar/attrib.ML	Tue Apr 05 13:07:40 2011 +0200
     9.2 +++ b/src/Pure/Isar/attrib.ML	Tue Apr 05 14:25:18 2011 +0200
     9.3 @@ -398,8 +398,8 @@
     9.4  (* theory setup *)
     9.5  
     9.6  val _ = Context.>> (Context.map_theory
     9.7 - (register_config Syntax.ast_trace_raw #>
     9.8 -  register_config Syntax.ast_stat_raw #>
     9.9 + (register_config Ast.ast_trace_raw #>
    9.10 +  register_config Ast.ast_stat_raw #>
    9.11    register_config Syntax.positions_raw #>
    9.12    register_config Syntax.show_brackets_raw #>
    9.13    register_config Syntax.show_sorts_raw #>

    10.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 13:07:40 2011 +0200
    10.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 14:25:18 2011 +0200
    10.3 @@ -117,7 +117,7 @@
    10.4    ML_Lex.read pos txt
    10.5    |> ML_Context.expression pos
    10.6      ("val parse_ast_translation: (string * (" ^ advancedT a ^
    10.7 -      "Syntax.ast list -> Syntax.ast)) list")
    10.8 +      "Ast.ast list -> Ast.ast)) list")
    10.9      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   10.10    |> Context.theory_map;
   10.11  
   10.12 @@ -141,7 +141,7 @@
   10.13    ML_Lex.read pos txt
   10.14    |> ML_Context.expression pos
   10.15      ("val print_ast_translation: (string * (" ^ advancedT a ^
   10.16 -      "Syntax.ast list -> Syntax.ast)) list")
   10.17 +      "Ast.ast list -> Ast.ast)) list")
   10.18      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   10.19    |> Context.theory_map;
   10.20  

    11.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 05 13:07:40 2011 +0200
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 05 14:25:18 2011 +0200
    11.3 @@ -1093,12 +1093,12 @@
    11.4  
    11.5  local
    11.6  
    11.7 -fun const_ast_tr intern ctxt [Syntax.Variable c] =
    11.8 +fun const_ast_tr intern ctxt [Ast.Variable c] =
    11.9        let
   11.10          val Const (c', _) = read_const_proper ctxt false c;
   11.11          val d = if intern then Syntax.mark_const c' else c;
   11.12 -      in Syntax.Constant d end
   11.13 -  | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
   11.14 +      in Ast.Constant d end
   11.15 +  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
   11.16  
   11.17  val typ = Simple_Syntax.read_typ;
   11.18  

    12.1 --- a/src/Pure/Isar/runtime.ML	Tue Apr 05 13:07:40 2011 +0200
    12.2 +++ b/src/Pure/Isar/runtime.ML	Tue Apr 05 14:25:18 2011 +0200
    12.3 @@ -72,9 +72,9 @@
    12.4          | Fail msg => [raised exn "Fail" [msg]]
    12.5          | THEORY (msg, thys) =>
    12.6              [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    12.7 -        | Syntax.AST (msg, asts) =>
    12.8 +        | Ast.AST (msg, asts) =>
    12.9              [raised exn "AST" (msg ::
   12.10 -              (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
   12.11 +              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
   12.12          | TYPE (msg, Ts, ts) =>
   12.13              [raised exn "TYPE" (msg ::
   12.14                (if detailed then

    13.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 13:07:40 2011 +0200
    13.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 14:25:18 2011 +0200
    13.3 @@ -71,17 +71,20 @@
    13.4    |> Sign.add_modesyntax_i ("latex", false)
    13.5        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
    13.6    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    13.7 -      [(Syntax.mk_appl (Constant "_Lam")
    13.8 -          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    13.9 -        Syntax.mk_appl (Constant "_Lam")
   13.10 -          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
   13.11 -       (Syntax.mk_appl (Constant "_Lam")
   13.12 -          [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
   13.13 -        Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
   13.14 -          (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
   13.15 -       (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
   13.16 -        Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
   13.17 -          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
   13.18 +      [(Ast.mk_appl (Ast.Constant "_Lam")
   13.19 +          [Ast.mk_appl (Ast.Constant "_Lam0")
   13.20 +            [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
   13.21 +        Ast.mk_appl (Ast.Constant "_Lam")
   13.22 +          [Ast.Variable "l",
   13.23 +            Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
   13.24 +       (Ast.mk_appl (Ast.Constant "_Lam")
   13.25 +          [Ast.mk_appl (Ast.Constant "_Lam1")
   13.26 +            [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
   13.27 +        Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
   13.28 +          (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
   13.29 +       (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
   13.30 +        Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
   13.31 +          [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
   13.32  
   13.33  
   13.34  (**** translation between proof terms and pure terms ****)

    14.1 --- a/src/Pure/Syntax/ast.ML	Tue Apr 05 13:07:40 2011 +0200
    14.2 +++ b/src/Pure/Syntax/ast.ML	Tue Apr 05 14:25:18 2011 +0200
    14.3 @@ -4,21 +4,18 @@
    14.4  Abstract syntax trees, translation rules, matching and normalization of asts.
    14.5  *)
    14.6  
    14.7 -signature AST0 =
    14.8 +signature AST =
    14.9  sig
   14.10    datatype ast =
   14.11      Constant of string |
   14.12      Variable of string |
   14.13      Appl of ast list
   14.14 +  val mk_appl: ast -> ast list -> ast
   14.15    exception AST of string * ast list
   14.16 -end;
   14.17 -
   14.18 -signature AST1 =
   14.19 -sig
   14.20 -  include AST0
   14.21 -  val mk_appl: ast -> ast list -> ast
   14.22    val pretty_ast: ast -> Pretty.T
   14.23    val pretty_rule: ast * ast -> Pretty.T
   14.24 +  val head_of_rule: ast * ast -> string
   14.25 +  val rule_error: ast * ast -> string option
   14.26    val fold_ast: string -> ast list -> ast
   14.27    val fold_ast_p: string -> ast list * ast -> ast
   14.28    val unfold_ast: string -> ast -> ast list
   14.29 @@ -27,17 +24,10 @@
   14.30    val ast_trace: bool Config.T
   14.31    val ast_stat_raw: Config.raw
   14.32    val ast_stat: bool Config.T
   14.33 -end;
   14.34 -
   14.35 -signature AST =
   14.36 -sig
   14.37 -  include AST1
   14.38 -  val head_of_rule: ast * ast -> string
   14.39 -  val rule_error: ast * ast -> string option
   14.40    val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
   14.41  end;
   14.42  
   14.43 -structure Ast : AST =
   14.44 +structure Ast: AST =
   14.45  struct
   14.46  
   14.47  (** abstract syntax trees **)
   14.48 @@ -53,16 +43,12 @@
   14.49    Variable of string |    (*x, ?x, 'a, ?'a*)
   14.50    Appl of ast list;       (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
   14.51  
   14.52 -
   14.53  (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
   14.54    there are no empty asts or nullary applications; use mk_appl for convenience*)
   14.55 -
   14.56  fun mk_appl f [] = f
   14.57    | mk_appl f args = Appl (f :: args);
   14.58  
   14.59 -
   14.60  (*exception for system errors involving asts*)
   14.61 -
   14.62  exception AST of string * ast list;
   14.63  
   14.64  

    15.1 --- a/src/Pure/Syntax/syntax.ML	Tue Apr 05 13:07:40 2011 +0200
    15.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Apr 05 14:25:18 2011 +0200
    15.3 @@ -7,7 +7,6 @@
    15.4  
    15.5  signature BASIC_SYNTAX =
    15.6  sig
    15.7 -  include AST0
    15.8    include SYN_TRANS0
    15.9    include MIXFIX0
   15.10    include PRINTER0
   15.11 @@ -15,7 +14,6 @@
   15.12  
   15.13  signature SYNTAX =
   15.14  sig
   15.15 -  include AST1
   15.16    include LEXICON0
   15.17    include SYN_EXT0
   15.18    include TYPE_EXT0
   15.19 @@ -129,7 +127,7 @@
   15.20      Parse_Print_Rule of 'a * 'a
   15.21    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   15.22    val is_const: syntax -> string -> bool
   15.23 -  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
   15.24 +  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> Ast.ast
   15.25    val standard_unparse_sort: {extern_class: string -> xstring} ->
   15.26      Proof.context -> syntax -> sort -> Pretty.T
   15.27    val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
   15.28 @@ -138,22 +136,22 @@
   15.29      {extern_class: string -> xstring, extern_type: string -> xstring,
   15.30        extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   15.31    val update_trfuns:
   15.32 -    (string * ((ast list -> ast) * stamp)) list *
   15.33 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   15.34      (string * ((term list -> term) * stamp)) list *
   15.35      (string * ((bool -> typ -> term list -> term) * stamp)) list *
   15.36 -    (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
   15.37 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   15.38    val update_advanced_trfuns:
   15.39 -    (string * ((Proof.context -> ast list -> ast) * stamp)) list *
   15.40 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   15.41      (string * ((Proof.context -> term list -> term) * stamp)) list *
   15.42      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   15.43 -    (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
   15.44 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   15.45    val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
   15.46      syntax -> syntax
   15.47    val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   15.48    val update_const_gram: bool -> (string -> bool) ->
   15.49      mode -> (string * typ * mixfix) list -> syntax -> syntax
   15.50 -  val update_trrules: ast trrule list -> syntax -> syntax
   15.51 -  val remove_trrules: ast trrule list -> syntax -> syntax
   15.52 +  val update_trrules: Ast.ast trrule list -> syntax -> syntax
   15.53 +  val remove_trrules: Ast.ast trrule list -> syntax -> syntax
   15.54  end;
   15.55  
   15.56  structure Syntax: SYNTAX =
   15.57 @@ -943,14 +941,13 @@
   15.58  
   15.59  
   15.60  (*export parts of internal Syntax structures*)
   15.61 -open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
   15.62 +open Lexicon Syn_Ext Parser Type_Ext Syn_Trans Mixfix Printer;
   15.63  
   15.64  end;
   15.65  
   15.66  structure Basic_Syntax: BASIC_SYNTAX = Syntax;
   15.67  open Basic_Syntax;
   15.68  
   15.69 -forget_structure "Ast";
   15.70  forget_structure "Syn_Ext";
   15.71  forget_structure "Parser";
   15.72  forget_structure "Type_Ext";

    16.1 --- a/src/Pure/pure_setup.ML	Tue Apr 05 13:07:40 2011 +0200
    16.2 +++ b/src/Pure/pure_setup.ML	Tue Apr 05 14:25:18 2011 +0200
    16.3 @@ -30,7 +30,7 @@
    16.4  toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    16.5  toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    16.6  toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    16.7 -toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
    16.8 +toplevel_pp ["Syntax", "ast"] "Ast.pretty_ast";
    16.9  toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
   16.10  toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
   16.11  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";

    17.1 --- a/src/Pure/sign.ML	Tue Apr 05 13:07:40 2011 +0200
    17.2 +++ b/src/Pure/sign.ML	Tue Apr 05 14:25:18 2011 +0200
    17.3 @@ -91,25 +91,25 @@
    17.4    val primitive_classrel: class * class -> theory -> theory
    17.5    val primitive_arity: arity -> theory -> theory
    17.6    val add_trfuns:
    17.7 -    (string * (ast list -> ast)) list *
    17.8 +    (string * (Ast.ast list -> Ast.ast)) list *
    17.9      (string * (term list -> term)) list *
   17.10      (string * (term list -> term)) list *
   17.11 -    (string * (ast list -> ast)) list -> theory -> theory
   17.12 +    (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
   17.13    val add_trfunsT:
   17.14      (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   17.15    val add_advanced_trfuns:
   17.16 -    (string * (Proof.context -> ast list -> ast)) list *
   17.17 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
   17.18      (string * (Proof.context -> term list -> term)) list *
   17.19      (string * (Proof.context -> term list -> term)) list *
   17.20 -    (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
   17.21 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   17.22    val add_advanced_trfunsT:
   17.23      (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   17.24    val add_tokentrfuns:
   17.25      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
   17.26    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
   17.27      -> theory -> theory
   17.28 -  val add_trrules: ast Syntax.trrule list -> theory -> theory
   17.29 -  val del_trrules: ast Syntax.trrule list -> theory -> theory
   17.30 +  val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   17.31 +  val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   17.32    val new_group: theory -> theory
   17.33    val reset_group: theory -> theory
   17.34    val add_path: string -> theory -> theory