authentic proof syntax;

--- a/src/Pure/Proof/proof_syntax.ML	Fri Feb 12 14:28:01 2010 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Sat Feb 13 23:16:06 2010 +0100
@@ -47,15 +47,15 @@
   |> Sign.root_path
   |> Sign.add_defsort_i []
   |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
-  |> Sign.add_consts_i
-      [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
-       (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
-       (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn),
-       (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
-       (Binding.name "Hyp", propT --> proofT, NoSyn),
-       (Binding.name "Oracle", propT --> proofT, NoSyn),
-       (Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
-       (Binding.name "MinProof", proofT, Delimfix "?")]
+  |> fold (snd oo Sign.declare_const)
+      [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
+       ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+       ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
+       ((Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT), NoSyn),
+       ((Binding.name "Hyp", propT --> proofT), NoSyn),
+       ((Binding.name "Oracle", propT --> proofT), NoSyn),
+       ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
+       ((Binding.name "MinProof", proofT), Delimfix "?")]
   |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
   |> Sign.add_syntax_i
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
@@ -65,10 +65,10 @@
        ("", paramT --> paramT, Delimfix "'(_')"),
        ("", idtT --> paramsT, Delimfix "_"),
        ("", paramT --> paramsT, Delimfix "_")]
-  |> Sign.add_modesyntax_i ("xsymbols", true)
+  |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
-       ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
-       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+       (Syntax.constN ^ "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
+       (Syntax.constN ^ "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
   |> Sign.add_modesyntax_i ("latex", false)
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
   |> Sign.add_trrules_i (map Syntax.ParsePrintRule
@@ -78,10 +78,10 @@
           [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 "AbsP") [Variable "A",
+        Syntax.mk_appl (Constant (Syntax.constN ^ "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 "Abst")
+        Syntax.mk_appl (Constant (Syntax.constN ^ "Abst"))
           [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);