1.1 --- a/src/HOL/Tools/refute.ML	Mon Aug 09 10:09:44 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Aug 09 15:27:27 2004 +0200
     1.3 @@ -616,7 +616,7 @@
     1.4  							  Type (s', _) =>
     1.5  								(case DatatypePackage.datatype_info thy s' of
     1.6  								  Some info =>
     1.7 -									(* TODO: I'm not quite sute if comparing the names is sufficient, or if *)
     1.8 +									(* TODO: I'm not quite sure if comparing the names is sufficient, or if *)
     1.9  									(*       we should also check the type                                  *)
    1.10  									s mem (#rec_names info)
    1.11  								| None =>  (* not an inductive datatype *)
    1.12 @@ -625,10 +625,18 @@
    1.13  								false)
    1.14  							handle LIST "last_elem" => false)  (* not even a function type *)
    1.15  				in
    1.16 -					if is_IDT_constructor () orelse is_IDT_recursor () then
    1.17 +					if is_IDT_constructor () then
    1.18  						(* only collect relevant type axioms *)
    1.19  						collect_type_axioms (axs, T)
    1.20 -					else
    1.21 +					else if is_IDT_recursor () then (
    1.22 +						(* TODO: we must add the definition of the recursion operator to the axioms, or *)
    1.23 +						(*       (better yet, since simply unfolding the definition won't work for      *)
    1.24 +						(*       initial fragments of recursive IDTs) write an interpreter that         *)
    1.25 +						(*       respects it                                                            *)
    1.26 +						warning "Term contains recursion over a datatype; countermodel(s) may be spurious!";
    1.27 +						(* only collect relevant type axioms *)
    1.28 +						collect_type_axioms (axs, T)
    1.29 +					) else
    1.30  						(case get_defn axioms of
    1.31  						  Some (axname, ax) => 
    1.32  							if mem_term (ax, axs) then