# HG changeset patch
# User wenzelm
# Date 1365021025 -7200
# Node ID 9c01df6a98434b2472f2c2a8ead6276ad2d9e6e5
# Parent  ee3398dfee9a4c1e1160ae7a7666e4148d012ae6
tuned;

diff -r ee3398dfee9a -r 9c01df6a9843 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Apr 03 22:05:24 2013 +0200
+++ b/src/Pure/goal.ML	Wed Apr 03 22:30:25 2013 +0200
@@ -95,10 +95,10 @@
    C
 *)
 fun check_finished ctxt th =
-  (case Thm.nprems_of th of
-    0 => th
-  | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
+  if Thm.no_prems th then th
+  else
+    raise THM ("Proof failed.\n" ^
+      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
@@ -184,7 +184,7 @@
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
 
 fun reset_futures () =
-  Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
+  Synchronized.change_result forked_proofs (fn (_, groups, _) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
 fun shutdown_futures () =