src/Pure/variable.ML

--- a/src/Pure/variable.ML	Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/variable.ML	Thu Jun 09 20:22:22 2011 +0200
@@ -391,7 +391,7 @@
 
 fun invent_types Ss ctxt =
   let
-    val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
     val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   in (tfrees, ctxt') end;