src/Pure/Proof/proof_syntax.ML
changeset 14854 61bdf2ae4dc5
parent 13530 4813fdc0ef17
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 11:25:26 2004 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 12:33:50 2004 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  val paramT = Type ("param", []);
     1.5  val paramsT = Type ("params", []);
     1.6  val idtT = Type ("idt", []);
     1.7 -val aT = TFree ("'a", ["logic"]);
     1.8 +val aT = TFree ("'a", []);
     1.9  
    1.10  (** constants for theorems and axioms **)
    1.11  
    1.12 @@ -49,9 +49,8 @@
    1.13    sg
    1.14    |> Sign.copy
    1.15    |> Sign.add_path "/"
    1.16 -  |> Sign.add_defsort_i ["logic"]
    1.17 +  |> Sign.add_defsort_i []
    1.18    |> Sign.add_types [("proof", 0, NoSyn)]
    1.19 -  |> Sign.add_arities [("proof", [], "logic")]
    1.20    |> Sign.add_consts_i
    1.21        [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    1.22         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),