# HG changeset patch
# User webertj
# Date 1092058047 -7200
# Node ID 5224130bc0d61e4dfe2c366bb18ef235ec172d93
# Parent  1d9b4fcd222dc472e50e3e390a394d1f0cf1abb4
warning for recursion over IDTs added

diff -r 1d9b4fcd222d -r 5224130bc0d6 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Aug 09 10:09:44 2004 +0200
+++ b/src/HOL/Tools/refute.ML	Mon Aug 09 15:27:27 2004 +0200
@@ -616,7 +616,7 @@
 							  Type (s', _) =>
 								(case DatatypePackage.datatype_info thy s' of
 								  Some info =>
-									(* TODO: I'm not quite sute if comparing the names is sufficient, or if *)
+									(* TODO: I'm not quite sure if comparing the names is sufficient, or if *)
 									(*       we should also check the type                                  *)
 									s mem (#rec_names info)
 								| None =>  (* not an inductive datatype *)
@@ -625,10 +625,18 @@
 								false)
 							handle LIST "last_elem" => false)  (* not even a function type *)
 				in
-					if is_IDT_constructor () orelse is_IDT_recursor () then
+					if is_IDT_constructor () then
 						(* only collect relevant type axioms *)
 						collect_type_axioms (axs, T)
-					else
+					else if is_IDT_recursor () then (
+						(* TODO: we must add the definition of the recursion operator to the axioms, or *)
+						(*       (better yet, since simply unfolding the definition won't work for      *)
+						(*       initial fragments of recursive IDTs) write an interpreter that         *)
+						(*       respects it                                                            *)
+						warning "Term contains recursion over a datatype; countermodel(s) may be spurious!";
+						(* only collect relevant type axioms *)
+						collect_type_axioms (axs, T)
+					) else
 						(case get_defn axioms of
 						  Some (axname, ax) => 
 							if mem_term (ax, axs) then