src/Pure/Proof/proof_syntax.ML

--- a/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 12:33:50 2004 +0200
@@ -34,7 +34,7 @@
 val paramT = Type ("param", []);
 val paramsT = Type ("params", []);
 val idtT = Type ("idt", []);
-val aT = TFree ("'a", ["logic"]);
+val aT = TFree ("'a", []);
 
 (** constants for theorems and axioms **)
 
@@ -49,9 +49,8 @@
   sg
   |> Sign.copy
   |> Sign.add_path "/"
-  |> Sign.add_defsort_i ["logic"]
+  |> Sign.add_defsort_i []
   |> Sign.add_types [("proof", 0, NoSyn)]
-  |> Sign.add_arities [("proof", [], "logic")]
   |> Sign.add_consts_i
       [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),