# HG changeset patch # User wenzelm # Date 1147777514 -7200 # Node ID c887656778bc541f1e258adcd27255e9b0a89990 # Parent 702843484da687c35a32f400af293c13dd7762ef Sign.certify_sort; diff -r 702843484da6 -r c887656778bc src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Tue May 16 13:01:31 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Tue May 16 13:05:14 2006 +0200 @@ -136,8 +136,6 @@ ProjectRule.projections rule |> map (standard #> RuleCases.save rule); -fun norm_sort thy = Sorts.norm_sort (snd (#classes (Type.rep_tsig (Sign.tsig_of thy)))); - fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = let (* this theory is used just for parsing *) @@ -1102,7 +1100,7 @@ val pnames = if length descr'' = 1 then ["P"] else map (fn i => "P" ^ string_of_int i) (1 upto length descr''); val ind_sort = if null dt_atomTs then HOLogic.typeS - else norm_sort thy9 (map (fn T => Sign.intern_class thy9 ("fs_" ^ + else Sign.certify_sort thy9 (map (fn T => Sign.intern_class thy9 ("fs_" ^ Sign.base_name (fst (dest_Type T)))) dt_atomTs); val fsT = TFree ("'n", ind_sort); val fsT' = TFree ("'n", HOLogic.typeS);