| changeset 14854 | 61bdf2ae4dc5 |
| parent 14787 | 724ce6e574e3 |
| child 14981 | e73f8140af78 |
--- a/src/Pure/proofterm.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/proofterm.ML Tue Jun 01 12:33:50 2004 +0200 @@ -685,8 +685,8 @@ (***** axioms for equality *****) -val aT = TFree ("'a", ["logic"]); -val bT = TFree ("'b", ["logic"]); +val aT = TFree ("'a", []); +val bT = TFree ("'b", []); val x = Free ("x", aT); val y = Free ("y", aT); val z = Free ("z", aT);