diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Thu Mar 02 12:07:20 1995 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Mar 03 11:48:05 1995 +0100
@@ -20,7 +20,6 @@
     val args: string
     val any: string
     val sprop: string
-    val applC: string
     val typ_to_nonterm: typ -> string
     datatype xsymb =
       Delim of string |
@@ -78,7 +77,6 @@
 val logicT = Type (logic, []);
 
 val args = "args";
-val argsT = Type (args, []);
 
 val typeT = Type ("type", []);
 
@@ -91,7 +89,6 @@
 
 (* constants *)
 
-val applC = "_appl";
 val constrainC = "_constrain";