src/HOL/Nominal/nominal_inductive.ML
changeset 43326 47cf4bc789aa
parent 42361 23f352990944
child 44045 2814ff2a6e3e
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4      val ind_sort = if null atomTs then HOLogic.typeS
     1.5        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     1.6          ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
     1.7 -    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
     1.8 +    val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     1.9      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    1.10      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    1.11