# HG changeset patch
# User webertj
# Date 1100705047 -3600
# Node ID 09e2188792652e9939d4a86bf96af0db0cd9869e
# Parent  dd4648ae6effc690963b1bfc6e1542ad52750ebb
minor changes (comments/code refactoring)

diff -r dd4648ae6eff -r 09e218879265 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Nov 17 07:35:50 2004 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Nov 17 16:24:07 2004 +0100
@@ -999,7 +999,7 @@
 
 
 (* ------------------------------------------------------------------------- *)
-(* INTERPRETERS                                                              *)
+(* INTERPRETERS: Auxiliary Functions                                         *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
@@ -1125,6 +1125,24 @@
 		Leaf [equal (i1, i2), not_equal (i1, i2)]
 	end;
 
+(* ------------------------------------------------------------------------- *)
+(* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
+(* ------------------------------------------------------------------------- *)
+
+	(* Term.term -> int -> Term.term *)
+
+	fun eta_expand t i =
+	let
+		val Ts = binder_types (fastype_of t)
+	in
+		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
+			(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
+	end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* INTERPRETERS: Actual Interpreters                                         *)
+(* ------------------------------------------------------------------------- *)
 
 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
 
@@ -1315,16 +1333,6 @@
 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
 
 	fun HOLogic_interpreter thy model args t =
-	let
-		(* Term.term -> int -> Term.term *)
-		fun eta_expand t i =
-		let
-			val Ts = binder_types (fastype_of t)
-		in
-			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
-				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
-		end
-	in
 	(* ------------------------------------------------------------------------- *)
 	(* Providing interpretations directly is more efficient than unfolding the   *)
 	(* logical constants.  In HOL however, logical constants can themselves be   *)
@@ -1340,7 +1348,11 @@
 			Some (TT, model, args)
 		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
 			Some (FF, model, args)
-		| Const ("All", _) $ t1 =>
+		| Const ("All", _) $ t1 =>  (* if 'All' occurs without an argument (i.e.   *)
+		                            (* as argument to a higher-order function or   *)
+		                            (* predicate), it is handled by the            *)
+		                            (* 'stlc_interpreter' (i.e. by unfolding its   *)
+		                            (* definition)                                 *)
 			let
 				val (i, m, a) = interpret thy model args t1
 			in
@@ -1353,9 +1365,13 @@
 						Some (Leaf [fmTrue, fmFalse], m, a)
 					end
 				| _ =>
-					raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
+					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
 			end
-		| Const ("Ex", _) $ t1 =>
+		| Const ("Ex", _) $ t1 =>  (* if 'Ex' occurs without an argument (i.e. as  *)
+		                           (* argument to a higher-order function or       *)
+		                           (* predicate), it is handled by the             *)
+		                           (* 'stlc_interpreter' (i.e. by unfolding its    *)
+		                           (* definition)                                  *)
 			let
 				val (i, m, a) = interpret thy model args t1
 			in
@@ -1368,7 +1384,7 @@
 						Some (Leaf [fmTrue, fmFalse], m, a)
 					end
 				| _ =>
-					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
+					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function")
 			end
 		| Const ("op =", _) $ t1 $ t2 =>
 			let
@@ -1387,8 +1403,7 @@
 			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
 		| Const ("op -->", _) =>
 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
-		| _ => None
-	end;
+		| _ => None;
 
 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
 
@@ -1396,14 +1411,6 @@
 	(* "T set" is isomorphic to "T --> bool" *)
 	let
 		val (typs, terms) = model
-		(* Term.term -> int -> Term.term *)
-		fun eta_expand t i =
-		let
-			val Ts = binder_types (fastype_of t)
-		in
-			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
-				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
-		end
 	in
 		case assoc (terms, t) of
 		  Some intr =>