--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:51:49 2011 +0200
@@ -226,7 +226,7 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
- val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);