Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed problem with strong induction theorem for datatypes containing
authorberghofe
Fri, 25 Nov 2005 14:00:22 +0100
changeset 18245 65e60434b3c2
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 file | annotate | diff | comparison | revisions 
--- 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 =
isabelle