# HG changeset patch
# User blanchet
# Date 1283281307 -7200
# Node ID 827c98e8ba8b8a3a7ea9e1bee780811cb8e9212c
# Parent  aea3d2566374b80006966ddd8ac1c6eae22d3fb7
fiddling with "try"

diff -r aea3d2566374 -r 827c98e8ba8b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 31 21:00:57 2010 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 31 21:01:47 2010 +0200
@@ -30,6 +30,7 @@
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
+  "Tools/try.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
diff -r aea3d2566374 -r 827c98e8ba8b src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Tue Aug 31 21:00:57 2010 +0200
+++ b/src/HOL/Tools/try.ML	Tue Aug 31 21:01:47 2010 +0200
@@ -6,23 +6,24 @@
 
 signature TRY =
 sig
-  val timeout : int Unsynchronized.ref
   val invoke_try : Proof.state -> unit
 end;
 
 structure Try : TRY =
 struct
 
-fun can_apply time pre post tac st =
+val timeout = Time.fromSeconds 5
+
+fun can_apply pre post tac st =
   let val {goal, ...} = Proof.goal st in
-    case TimeLimit.timeLimit time (Seq.pull o tac) (pre st) of
+    case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
       SOME (x, _) => nprems_of (post x) < nprems_of goal
     | NONE => false
   end
 
-fun do_generic command timeout pre post apply st =
+fun do_generic command pre post apply st =
   let val timer = Timer.startRealTimer () in
-    if can_apply timeout pre post apply st then
+    if can_apply pre post apply st then
       SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
     else
       NONE
@@ -36,8 +37,8 @@
     Method.apply (named_method thy name) ctxt []
   end
 
-fun do_named_method name timeout st =
-  do_generic name timeout (#goal o Proof.goal) snd
+fun do_named_method name st =
+  do_generic name (#goal o Proof.goal) snd
              (apply_named_method name (Proof.context_of st)) st
 
 fun apply_named_method_on_first_goal name ctxt =
@@ -45,9 +46,9 @@
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name timeout st =
+fun do_named_method_on_first_goal name st =
   do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
-                      else "")) timeout I (#goal o Proof.goal)
+                      else "")) I (#goal o Proof.goal)
              (apply_named_method_on_first_goal name (Proof.context_of st)) st
 
 val all_goals_named_methods = ["auto", "safe"]
@@ -59,12 +60,10 @@
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
 
-val timeout = Unsynchronized.ref 5
-
 fun invoke_try st =
-  case do_methods |> Par_List.map (fn f => f (Time.fromSeconds (!timeout)) st)
+  case do_methods |> Par_List.map (fn f => f st)
                   |> map_filter I |> sort (int_ord o pairself snd) of
-    [] => writeln "Tried."
+    [] => writeln "No proof found."
   | xs as (s, _) :: _ =>
     priority ("Try this command: " ^
               Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^