1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Feb 12 14:28:01 2010 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
     1.3 @@ -47,15 +47,15 @@
     1.4    |> Sign.root_path
     1.5    |> Sign.add_defsort_i []
     1.6    |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
     1.7 -  |> Sign.add_consts_i
     1.8 -      [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
     1.9 -       (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    1.10 -       (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn),
    1.11 -       (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
    1.12 -       (Binding.name "Hyp", propT --> proofT, NoSyn),
    1.13 -       (Binding.name "Oracle", propT --> proofT, NoSyn),
    1.14 -       (Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
    1.15 -       (Binding.name "MinProof", proofT, Delimfix "?")]
    1.16 +  |> fold (snd oo Sign.declare_const)
    1.17 +      [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
    1.18 +       ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    1.19 +       ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
    1.20 +       ((Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT), NoSyn),
    1.21 +       ((Binding.name "Hyp", propT --> proofT), NoSyn),
    1.22 +       ((Binding.name "Oracle", propT --> proofT), NoSyn),
    1.23 +       ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
    1.24 +       ((Binding.name "MinProof", proofT), Delimfix "?")]
    1.25    |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
    1.26    |> Sign.add_syntax_i
    1.27        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    1.28 @@ -65,10 +65,10 @@
    1.29         ("", paramT --> paramT, Delimfix "'(_')"),
    1.30         ("", idtT --> paramsT, Delimfix "_"),
    1.31         ("", paramT --> paramsT, Delimfix "_")]
    1.32 -  |> Sign.add_modesyntax_i ("xsymbols", true)
    1.33 +  |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    1.34        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    1.35 -       ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    1.36 -       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    1.37 +       (Syntax.constN ^ "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    1.38 +       (Syntax.constN ^ "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    1.39    |> Sign.add_modesyntax_i ("latex", false)
    1.40        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
    1.41    |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    1.42 @@ -78,10 +78,10 @@
    1.43            [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    1.44         (Syntax.mk_appl (Constant "_Lam")
    1.45            [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    1.46 -        Syntax.mk_appl (Constant "AbsP") [Variable "A",
    1.47 +        Syntax.mk_appl (Constant (Syntax.constN ^ "AbsP")) [Variable "A",
    1.48            (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    1.49         (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    1.50 -        Syntax.mk_appl (Constant "Abst")
    1.51 +        Syntax.mk_appl (Constant (Syntax.constN ^ "Abst"))
    1.52            [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    1.53  
    1.54