1.1 --- a/src/HOL/Tools/refute.ML	Wed Nov 17 07:35:50 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Nov 17 16:24:07 2004 +0100
     1.3 @@ -999,7 +999,7 @@
     1.4  
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* INTERPRETERS                                                              *)
     1.8 +(* INTERPRETERS: Auxiliary Functions                                         *)
     1.9  (* ------------------------------------------------------------------------- *)
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 @@ -1125,6 +1125,24 @@
    1.13  		Leaf [equal (i1, i2), not_equal (i1, i2)]
    1.14  	end;
    1.15  
    1.16 +(* ------------------------------------------------------------------------- *)
    1.17 +(* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
    1.18 +(* ------------------------------------------------------------------------- *)
    1.19 +
    1.20 +	(* Term.term -> int -> Term.term *)
    1.21 +
    1.22 +	fun eta_expand t i =
    1.23 +	let
    1.24 +		val Ts = binder_types (fastype_of t)
    1.25 +	in
    1.26 +		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
    1.27 +			(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
    1.28 +	end;
    1.29 +
    1.30 +
    1.31 +(* ------------------------------------------------------------------------- *)
    1.32 +(* INTERPRETERS: Actual Interpreters                                         *)
    1.33 +(* ------------------------------------------------------------------------- *)
    1.34  
    1.35  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.36  
    1.37 @@ -1315,16 +1333,6 @@
    1.38  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.39  
    1.40  	fun HOLogic_interpreter thy model args t =
    1.41 -	let
    1.42 -		(* Term.term -> int -> Term.term *)
    1.43 -		fun eta_expand t i =
    1.44 -		let
    1.45 -			val Ts = binder_types (fastype_of t)
    1.46 -		in
    1.47 -			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
    1.48 -				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
    1.49 -		end
    1.50 -	in
    1.51  	(* ------------------------------------------------------------------------- *)
    1.52  	(* Providing interpretations directly is more efficient than unfolding the   *)
    1.53  	(* logical constants.  In HOL however, logical constants can themselves be   *)
    1.54 @@ -1340,7 +1348,11 @@
    1.55  			Some (TT, model, args)
    1.56  		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
    1.57  			Some (FF, model, args)
    1.58 -		| Const ("All", _) $ t1 =>
    1.59 +		| Const ("All", _) $ t1 =>  (* if 'All' occurs without an argument (i.e.   *)
    1.60 +		                            (* as argument to a higher-order function or   *)
    1.61 +		                            (* predicate), it is handled by the            *)
    1.62 +		                            (* 'stlc_interpreter' (i.e. by unfolding its   *)
    1.63 +		                            (* definition)                                 *)
    1.64  			let
    1.65  				val (i, m, a) = interpret thy model args t1
    1.66  			in
    1.67 @@ -1353,9 +1365,13 @@
    1.68  						Some (Leaf [fmTrue, fmFalse], m, a)
    1.69  					end
    1.70  				| _ =>
    1.71 -					raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
    1.72 +					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
    1.73  			end
    1.74 -		| Const ("Ex", _) $ t1 =>
    1.75 +		| Const ("Ex", _) $ t1 =>  (* if 'Ex' occurs without an argument (i.e. as  *)
    1.76 +		                           (* argument to a higher-order function or       *)
    1.77 +		                           (* predicate), it is handled by the             *)
    1.78 +		                           (* 'stlc_interpreter' (i.e. by unfolding its    *)
    1.79 +		                           (* definition)                                  *)
    1.80  			let
    1.81  				val (i, m, a) = interpret thy model args t1
    1.82  			in
    1.83 @@ -1368,7 +1384,7 @@
    1.84  						Some (Leaf [fmTrue, fmFalse], m, a)
    1.85  					end
    1.86  				| _ =>
    1.87 -					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
    1.88 +					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function")
    1.89  			end
    1.90  		| Const ("op =", _) $ t1 $ t2 =>
    1.91  			let
    1.92 @@ -1387,8 +1403,7 @@
    1.93  			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
    1.94  		| Const ("op -->", _) =>
    1.95  			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
    1.96 -		| _ => None
    1.97 -	end;
    1.98 +		| _ => None;
    1.99  
   1.100  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.101  
   1.102 @@ -1396,14 +1411,6 @@
   1.103  	(* "T set" is isomorphic to "T --> bool" *)
   1.104  	let
   1.105  		val (typs, terms) = model
   1.106 -		(* Term.term -> int -> Term.term *)
   1.107 -		fun eta_expand t i =
   1.108 -		let
   1.109 -			val Ts = binder_types (fastype_of t)
   1.110 -		in
   1.111 -			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   1.112 -				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
   1.113 -		end
   1.114  	in
   1.115  		case assoc (terms, t) of
   1.116  		  Some intr =>