src/Pure/Isar/locale.ML
changeset 14695 9c78044b99c3
parent 14643 130076a81b84
child 14777 5bb4bbdb6529
--- a/src/Pure/Isar/locale.ML	Sat May 01 22:07:16 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Sat May 01 22:08:57 2004 +0200
@@ -476,7 +476,7 @@
   let
     val tvars = rev (foldl Term.add_tvarsT ([], Ts));
     val tfrees = map TFree
-      (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars);
+      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
   in map #1 tvars ~~ tfrees end;
 
 fun unify_frozen ctxt maxidx Ts Us =