src/HOL/Nominal/nominal_package.ML
changeset 18245 65e60434b3c2
parent 18142 a51ab4152097
child 18246 676d2e625d98
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 11:34:37 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 14:00:22 2005 +0100
     1.3 @@ -1022,8 +1022,9 @@
     1.4  
     1.5      val pnames = if length descr'' = 1 then ["P"]
     1.6        else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
     1.7 -    val ind_sort = map (fn T => Sign.intern_class thy8 ("fs_" ^
     1.8 -      Sign.base_name (fst (dest_Type T)))) dt_atomTs;
     1.9 +    val ind_sort = if null dt_atomTs then HOLogic.typeS
    1.10 +      else map (fn T => Sign.intern_class thy8 ("fs_" ^
    1.11 +        Sign.base_name (fst (dest_Type T)))) dt_atomTs;
    1.12      val fsT = TFree ("'n", ind_sort);
    1.13  
    1.14      fun make_pred i T =