--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 10:45:03 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 11:06:39 2014 +0100
@@ -54,7 +54,7 @@
((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
((Binding.name "MinProof", proofT), Delimfix "?")]
|> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
- |> Sign.add_syntax
+ |> Sign.add_syntax Syntax.mode_default
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
@@ -62,7 +62,7 @@
("", paramT --> paramT, Delimfix "'(_')"),
("", idtT --> paramsT, Delimfix "_"),
("", paramT --> paramsT, Delimfix "_")]
- |> Sign.add_modesyntax (Symbol.xsymbolsN, true)
+ |> Sign.add_syntax (Symbol.xsymbolsN, true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
(Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
(Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]