src/HOL/Tools/refute.ML
changeset 18760 97aaecb84afe
parent 18708 4b3dadb4fe33
child 18932 66ecb05f92c8
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Jan 23 15:23:31 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jan 23 17:29:52 2006 +0100
     1.3 @@ -923,8 +923,6 @@
     1.4  (* {...}     : parameters that control the translation/model generation      *)
     1.5  (* t         : term to be translated into a propositional formula            *)
     1.6  (* negate    : if true, find a model that makes 't' false (rather than true) *)
     1.7 -(* Note: exception 'TimeOut' is raised if the algorithm does not terminate   *)
     1.8 -(*       within 'maxtime' seconds (if 'maxtime' >0)                          *)
     1.9  (* ------------------------------------------------------------------------- *)
    1.10  
    1.11  	(* theory -> params -> Term.term -> bool -> unit *)
    1.12 @@ -1014,9 +1012,9 @@
    1.13  			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
    1.14  				^ Sign.string_of_term (sign_of thy) t);
    1.15  			if maxtime>0 then (
    1.16 -				TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
    1.17 +				interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))
    1.18  					wrapper ()
    1.19 -				handle TimeLimit.TimeOut =>
    1.20 +				handle Interrupt =>
    1.21  					writeln ("\nSearch terminated, time limit ("
    1.22  						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
    1.23  						^ ") exceeded.")