src/HOL/Tools/refute.ML
changeset 30349 110826d1e5ff
parent 30347 91f73b2997f9
child 30450 7655e6533209
equal deleted inserted replaced
30348:5598523c482a 30349:110826d1e5ff
  1163     expect} t negate =
  1163     expect} t negate =
  1164   let
  1164   let
  1165     (* unit -> unit *)
  1165     (* unit -> unit *)
  1166     fun wrapper () =
  1166     fun wrapper () =
  1167     let
  1167     let
       
  1168       val timer  = Timer.startRealTimer ()
  1168       val u      = unfold_defs thy t
  1169       val u      = unfold_defs thy t
  1169       val _      = Output.tracing ("Unfolded term: " ^
  1170       val _      = Output.tracing ("Unfolded term: " ^
  1170                                    Syntax.string_of_term_global thy u)
  1171                                    Syntax.string_of_term_global thy u)
  1171       val axioms = collect_axioms thy u
  1172       val axioms = collect_axioms thy u
  1172       (* Term.typ list *)
  1173       (* Term.typ list *)
  1199         else
  1200         else
  1200           ()
  1201           ()
  1201       (* (Term.typ * int) list -> string *)
  1202       (* (Term.typ * int) list -> string *)
  1202       fun find_model_loop universe =
  1203       fun find_model_loop universe =
  1203       let
  1204       let
       
  1205         val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
       
  1206         val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
       
  1207                 orelse raise TimeLimit.TimeOut
  1204         val init_model = (universe, [])
  1208         val init_model = (universe, [])
  1205         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
  1209         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
  1206           bounds = [], wellformed = True}
  1210           bounds = [], wellformed = True}
  1207         val _          = Output.tracing ("Translating term (sizes: "
  1211         val _          = Output.tracing ("Translating term (sizes: "
  1208           ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
  1212           ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")