# HG changeset patch
# User paulson
# Date 1117009987 -7200
# Node ID 794b37d08a2e70e1e927381f2d1dcf6640f9cda1
# Parent  d8a6afbb71ecb6d4dad081dba0fa1ddd01e824a5
SML/NJ compatibility

diff -r d8a6afbb71ec -r 794b37d08a2e src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed May 25 10:32:20 2005 +0200
+++ b/src/HOL/Tools/refute.ML	Wed May 25 10:33:07 2005 +0200
@@ -2341,7 +2341,7 @@
 	fun Gfp_gfp_interpreter thy model args t =
 		case t of
 		  Const ("Gfp.gfp", Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) =>
-			let
+			let nonfix union (*because "union" is used below*)
 				val (i_elem, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
 				val size_elem      = size_of_type i_elem
 				(* the universe (i.e. the set that contains every element) *)
@@ -2360,16 +2360,16 @@
 					raise REFUTE ("Gfp_gfp_interpreter", "is_subset: interpretation for set is not a node")
 				(* interpretation * interpretation -> interpretation *)
 				fun union (Node xs, Node ys) =
-					Node (map (fn (x, y) => if (x = TT) orelse (y = TT) then TT else FF) (xs ~~ ys))
+					  Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF) 
+					       (xs ~~ ys))
 				  | union (_, _) =
 					raise REFUTE ("Lfp_lfp_interpreter", "union: interpretation for set is not a node")
 				(* interpretation -> interpretaion *)
 				fun gfp (Node resultsets) =
 					foldl (fn ((set, resultset), acc) =>
-						if is_subset (set, resultset) then
-							union (acc, set)
-						else
-							acc) i_univ (i_sets ~~ resultsets)
+						   if is_subset (set, resultset) then union (acc, set)
+						   else acc) 
+				  	      i_univ  (i_sets ~~ resultsets)
 				  | gfp _ =
 						raise REFUTE ("Gfp_gfp_interpreter", "gfp: interpretation for function is not a node")
 			in