SML/NJ compatibility
authorpaulson
Wed May 25 10:33:07 2005 +0200 (2005-05-25 ago)
changeset 16073794b37d08a2e
parent 16072 d8a6afbb71ec
child 16074 9e569163ba8c
SML/NJ compatibility
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed May 25 10:32:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed May 25 10:33:07 2005 +0200
     1.3 @@ -2341,7 +2341,7 @@
     1.4  	fun Gfp_gfp_interpreter thy model args t =
     1.5  		case t of
     1.6  		  Const ("Gfp.gfp", Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) =>
     1.7 -			let
     1.8 +			let nonfix union (*because "union" is used below*)
     1.9  				val (i_elem, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.10  				val size_elem      = size_of_type i_elem
    1.11  				(* the universe (i.e. the set that contains every element) *)
    1.12 @@ -2360,16 +2360,16 @@
    1.13  					raise REFUTE ("Gfp_gfp_interpreter", "is_subset: interpretation for set is not a node")
    1.14  				(* interpretation * interpretation -> interpretation *)
    1.15  				fun union (Node xs, Node ys) =
    1.16 -					Node (map (fn (x, y) => if (x = TT) orelse (y = TT) then TT else FF) (xs ~~ ys))
    1.17 +					  Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF) 
    1.18 +					       (xs ~~ ys))
    1.19  				  | union (_, _) =
    1.20  					raise REFUTE ("Lfp_lfp_interpreter", "union: interpretation for set is not a node")
    1.21  				(* interpretation -> interpretaion *)
    1.22  				fun gfp (Node resultsets) =
    1.23  					foldl (fn ((set, resultset), acc) =>
    1.24 -						if is_subset (set, resultset) then
    1.25 -							union (acc, set)
    1.26 -						else
    1.27 -							acc) i_univ (i_sets ~~ resultsets)
    1.28 +						   if is_subset (set, resultset) then union (acc, set)
    1.29 +						   else acc) 
    1.30 +				  	      i_univ  (i_sets ~~ resultsets)
    1.31  				  | gfp _ =
    1.32  						raise REFUTE ("Gfp_gfp_interpreter", "gfp: interpretation for function is not a node")
    1.33  			in