--- 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)),