Sign.certify_sort;
authorwenzelm
Tue May 16 13:05:14 2006 +0200 (2006-05-16)
changeset 19649c887656778bc
parent 19648 702843484da6
child 19650 33a94c5fc7bb
Sign.certify_sort;
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue May 16 13:01:31 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue May 16 13:05:14 2006 +0200
     1.3 @@ -136,8 +136,6 @@
     1.4    ProjectRule.projections rule
     1.5    |> map (standard #> RuleCases.save rule);
     1.6  
     1.7 -fun norm_sort thy = Sorts.norm_sort (snd (#classes (Type.rep_tsig (Sign.tsig_of thy))));
     1.8 -
     1.9  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
    1.10    let
    1.11      (* this theory is used just for parsing *)
    1.12 @@ -1102,7 +1100,7 @@
    1.13      val pnames = if length descr'' = 1 then ["P"]
    1.14        else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
    1.15      val ind_sort = if null dt_atomTs then HOLogic.typeS
    1.16 -      else norm_sort thy9 (map (fn T => Sign.intern_class thy9 ("fs_" ^
    1.17 +      else Sign.certify_sort thy9 (map (fn T => Sign.intern_class thy9 ("fs_" ^
    1.18          Sign.base_name (fst (dest_Type T)))) dt_atomTs);
    1.19      val fsT = TFree ("'n", ind_sort);
    1.20      val fsT' = TFree ("'n", HOLogic.typeS);