src/HOL/Nominal/nominal_inductive.ML
changeset 36428 874843c1e96e
parent 36323 655e2d74de3a
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Apr 27 19:44:04 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Apr 27 21:34:22 2010 +0200
     1.3 @@ -198,8 +198,8 @@
     1.4  
     1.5      val atomTs = distinct op = (maps (map snd o #2) prems);
     1.6      val ind_sort = if null atomTs then HOLogic.typeS
     1.7 -      else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     1.8 -        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
     1.9 +      else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    1.10 +        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
    1.11      val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    1.12      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    1.13      val fsT = TFree (fs_ctxt_tyname, ind_sort);