src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -99,7 +99,7 @@
 fun fixed_judgment thy x =
   let  (*be robust wrt. low-level errors*)
     val c = judgment_name thy;
-    val aT = TFree ("'a", []);
+    val aT = TFree (Name.aT, []);
     val T =
       the_default (aT --> propT) (Sign.const_type thy c)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));