src/HOL/Library/refute.ML
changeset 58843 521cea5fa777
parent 58825 2065f49da190
child 58893 9e0ecb66d6a7
     1.1 --- a/src/HOL/Library/refute.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -1068,31 +1068,31 @@
     1.4                              ". Available solvers: " ^
     1.5                              commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
     1.6            in
     1.7 -            Output.urgent_message "Invoking SAT solver...";
     1.8 +            writeln "Invoking SAT solver...";
     1.9              (case solver fm of
    1.10                SAT_Solver.SATISFIABLE assignment =>
    1.11 -                (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
    1.12 +                (writeln ("Model found:\n" ^ print_model ctxt model
    1.13                    (fn i => case assignment i of SOME b => b | NONE => true));
    1.14                   if maybe_spurious then "potential" else "genuine")
    1.15              | SAT_Solver.UNSATISFIABLE _ =>
    1.16 -                (Output.urgent_message "No model exists.";
    1.17 +                (writeln "No model exists.";
    1.18                  case next_universe universe sizes minsize maxsize of
    1.19                    SOME universe' => find_model_loop universe'
    1.20 -                | NONE => (Output.urgent_message
    1.21 +                | NONE => (writeln
    1.22                      "Search terminated, no larger universe within the given limits.";
    1.23                      "none"))
    1.24              | SAT_Solver.UNKNOWN =>
    1.25 -                (Output.urgent_message "No model found.";
    1.26 +                (writeln "No model found.";
    1.27                  case next_universe universe sizes minsize maxsize of
    1.28                    SOME universe' => find_model_loop universe'
    1.29 -                | NONE => (Output.urgent_message
    1.30 +                | NONE => (writeln
    1.31                    "Search terminated, no larger universe within the given limits.";
    1.32                    "unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
    1.33                (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
    1.34                 "unknown")
    1.35            end
    1.36            handle MAXVARS_EXCEEDED =>
    1.37 -            (Output.urgent_message ("Search terminated, number of Boolean variables ("
    1.38 +            (writeln ("Search terminated, number of Boolean variables ("
    1.39                ^ string_of_int maxvars ^ " allowed) exceeded.");
    1.40                "unknown")
    1.41  
    1.42 @@ -1114,14 +1114,14 @@
    1.43      maxtime>=0 orelse
    1.44        error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
    1.45      (* enter loop with or without time limit *)
    1.46 -    Output.urgent_message ("Trying to find a model that "
    1.47 +    writeln ("Trying to find a model that "
    1.48        ^ (if negate then "refutes" else "satisfies") ^ ": "
    1.49        ^ Syntax.string_of_term ctxt t);
    1.50      if maxtime > 0 then (
    1.51        TimeLimit.timeLimit (Time.fromSeconds maxtime)
    1.52          wrapper ()
    1.53        handle TimeLimit.TimeOut =>
    1.54 -        (Output.urgent_message ("Search terminated, time limit (" ^
    1.55 +        (writeln ("Search terminated, time limit (" ^
    1.56              string_of_int maxtime
    1.57              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
    1.58           check_expect "unknown")
    1.59 @@ -1207,7 +1207,7 @@
    1.60      val t = th |> prop_of
    1.61    in
    1.62      if Logic.count_prems t = 0 then
    1.63 -      (Output.urgent_message "No subgoal!"; "none")
    1.64 +      (writeln "No subgoal!"; "none")
    1.65      else
    1.66        let
    1.67          val assms = map term_of (Assumption.all_assms_of ctxt)