1.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 13:07:40 2011 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 05 14:25:18 2011 +0200
     1.3 @@ -71,17 +71,20 @@
     1.4    |> Sign.add_modesyntax_i ("latex", false)
     1.5        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
     1.6    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
     1.7 -      [(Syntax.mk_appl (Constant "_Lam")
     1.8 -          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
     1.9 -        Syntax.mk_appl (Constant "_Lam")
    1.10 -          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    1.11 -       (Syntax.mk_appl (Constant "_Lam")
    1.12 -          [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    1.13 -        Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
    1.14 -          (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    1.15 -       (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    1.16 -        Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
    1.17 -          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    1.18 +      [(Ast.mk_appl (Ast.Constant "_Lam")
    1.19 +          [Ast.mk_appl (Ast.Constant "_Lam0")
    1.20 +            [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
    1.21 +        Ast.mk_appl (Ast.Constant "_Lam")
    1.22 +          [Ast.Variable "l",
    1.23 +            Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
    1.24 +       (Ast.mk_appl (Ast.Constant "_Lam")
    1.25 +          [Ast.mk_appl (Ast.Constant "_Lam1")
    1.26 +            [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
    1.27 +        Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
    1.28 +          (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
    1.29 +       (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
    1.30 +        Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
    1.31 +          [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
    1.32  
    1.33  
    1.34  (**** translation between proof terms and pure terms ****)