src/Pure/Isar/specification.ML
changeset 24848 5dbbd33c3236
parent 24734 ff617b6711f4
child 24927 48e08f37ce92
--- 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)