diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/proofterm.ML
--- 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);