diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -45,8 +45,8 @@
   |> Theory.copy
   |> Sign.root_path
   |> Sign.set_defsort []
-  |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
-  |> fold (snd oo Sign.declare_const)
+  |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
+  |> fold (snd oo Sign.declare_const_global)
       [((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),
@@ -55,7 +55,7 @@
        ((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_nonterminals_global [Binding.name "param", Binding.name "params"]
   |> Sign.add_syntax_i
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),