src/HOL/Nominal/nominal_inductive.ML
changeset 56253 83b3c110f22d
parent 54991 1169c65e9698
child 57884 36b5691b81a5
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 18:15:09 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 18:16:54 2014 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4        end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
     1.5  
     1.6      val atomTs = distinct op = (maps (map snd o #2) prems);
     1.7 -    val ind_sort = if null atomTs then HOLogic.typeS
     1.8 +    val ind_sort = if null atomTs then @{sort type}
     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.variant "'n" (Variable.names_of ctxt');
    1.12 @@ -332,7 +332,7 @@
    1.13                   fun concat_perm pi1 pi2 =
    1.14                     let val T = fastype_of pi1
    1.15                     in if T = fastype_of pi2 then
    1.16 -                       Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
    1.17 +                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
    1.18                       else pi2
    1.19                     end;
    1.20                   val pis'' = fold (concat_perm #> map) pis' pis;