# HG changeset patch
# User berghofe
# Date 1132923622 -3600
# Node ID 65e60434b3c241684ab13a2ebbb4ddc294bc3af0
# Parent  694648741d5aac39520562e2bb09cd90baf9cf77
Fixed problem with strong induction theorem for datatypes containing
no atom types (ind_sort was the empty sort in this case).

diff -r 694648741d5a -r 65e60434b3c2 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 11:34:37 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 14:00:22 2005 +0100
@@ -1022,8 +1022,9 @@
 
     val pnames = if length descr'' = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
-    val ind_sort = map (fn T => Sign.intern_class thy8 ("fs_" ^
-      Sign.base_name (fst (dest_Type T)))) dt_atomTs;
+    val ind_sort = if null dt_atomTs then HOLogic.typeS
+      else map (fn T => Sign.intern_class thy8 ("fs_" ^
+        Sign.base_name (fst (dest_Type T)))) dt_atomTs;
     val fsT = TFree ("'n", ind_sort);
 
     fun make_pred i T =