src/Pure/Proof/proof_syntax.ML

   |> Sign.root_path
   |> Sign.set_defsort []
   |> Sign.add_nonterminals_global
     [Binding.make ("param", \<^here>),
      Binding.make ("params", \<^here>)]
-  |> Sign.syntax true Syntax.mode_default
+  |> Sign.syntax_global true Syntax.mode_default
     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
      ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
      ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
      ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
      ("", paramT --> paramT, Mixfix.mixfix "'(_')"),