diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -89,7 +89,7 @@
       (case duplicates (op =) commons of [] => ()
       | dups => error ("Duplicate local variables " ^ commas_quote dups));
     val frees = rev ((fold o fold_aterms) add_free As (rev commons));
-    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context "'a" (length frees));
+    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
 
     fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)