Fixed problem with strong induction theorem for datatypes containing
authorberghofe
Fri Nov 25 14:00:22 2005 +0100 (2005-11-25)
changeset 1824565e60434b3c2
parent 18244 694648741d5a
child 18246 676d2e625d98
Fixed problem with strong induction theorem for datatypes containing
no atom types (ind_sort was the empty sort in this case).
src/HOL/Nominal/nominal_package.ML
     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 =