src/HOL/Tools/refute.ML
changeset 15333 77b2bca7fcb5
parent 15292 09e218879265
child 15334 d5a92997dc1b
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Nov 25 14:44:52 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Nov 25 19:04:32 2004 +0100
     1.3 @@ -607,12 +607,8 @@
     1.4  							((case last_elem (binder_types T) of
     1.5  							  Type (s', _) =>
     1.6  								(case DatatypePackage.datatype_info thy s' of
     1.7 -								  Some info =>
     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 -									false)
    1.13 +								  Some info => s mem (#rec_names info)
    1.14 +								| None      => false)  (* not an inductive datatype *)
    1.15  							| _ =>  (* a (free or schematic) type variable *)
    1.16  								false)
    1.17  							handle LIST "last_elem" => false)  (* not even a function type *)
    1.18 @@ -1348,11 +1344,10 @@
    1.19  			Some (TT, model, args)
    1.20  		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
    1.21  			Some (FF, model, args)
    1.22 -		| Const ("All", _) $ t1 =>  (* if 'All' occurs without an argument (i.e.   *)
    1.23 -		                            (* as argument to a higher-order function or   *)
    1.24 -		                            (* predicate), it is handled by the            *)
    1.25 -		                            (* 'stlc_interpreter' (i.e. by unfolding its   *)
    1.26 -		                            (* definition)                                 *)
    1.27 +		| Const ("All", _) $ t1 =>
    1.28 +		(* if "All" occurs without an argument (i.e. as argument to a higher-order *)
    1.29 +		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
    1.30 +		(* by unfolding its definition)                                            *)
    1.31  			let
    1.32  				val (i, m, a) = interpret thy model args t1
    1.33  			in
    1.34 @@ -1367,11 +1362,10 @@
    1.35  				| _ =>
    1.36  					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
    1.37  			end
    1.38 -		| Const ("Ex", _) $ t1 =>  (* if 'Ex' occurs without an argument (i.e. as  *)
    1.39 -		                           (* argument to a higher-order function or       *)
    1.40 -		                           (* predicate), it is handled by the             *)
    1.41 -		                           (* 'stlc_interpreter' (i.e. by unfolding its    *)
    1.42 -		                           (* definition)                                  *)
    1.43 +		| Const ("Ex", _) $ t1 =>
    1.44 +		(* if "Ex" occurs without an argument (i.e. as argument to a higher-order  *)
    1.45 +		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
    1.46 +		(* by unfolding its definition)                                            *)
    1.47  			let
    1.48  				val (i, m, a) = interpret thy model args t1
    1.49  			in