diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 12:28:02 2019 +0200
@@ -28,7 +28,7 @@
 val paramT = Type ("param", []);
 val paramsT = Type ("params", []);
 val idtT = Type ("idt", []);
-val aT = TFree (Name.aT, []);
+val aT = Term.aT [];
 
 
 (** constants for theorems and axioms **)