# HG changeset patch
# User wenzelm
# Date 1434009834 -7200
# Node ID 051b102aa1e1f0c5d8d6df85bbc82b1663d67ccc
# Parent  eb3094c6576c756f1c6f1cac6e3da0a76159e70d
tuned;

diff -r eb3094c6576c -r 051b102aa1e1 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Jun 11 00:13:25 2015 +0100
+++ b/src/Pure/Isar/object_logic.ML	Thu Jun 11 10:03:54 2015 +0200
@@ -125,7 +125,7 @@
     val aT = TFree (Name.aT, []);
     val T =
       the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
-      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
+      |> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;