# HG changeset patch
# User wenzelm
# Date 1361467648 -3600
# Node ID 22ba938ab10f15463cc591c4c96e027185d7145a
# Parent  1f614b4eb36796f363f1517e8b7aa5fee44fc88e# Parent  f301ad90c48b87670429d180a2b42bae1566a86d
merged

diff -r 1f614b4eb367 -r 22ba938ab10f .hgtags
--- a/.hgtags	Thu Feb 21 16:36:19 2013 +0100
+++ b/.hgtags	Thu Feb 21 18:27:28 2013 +0100
@@ -5,7 +5,6 @@
 23ceb1dc9755a8ad6f0230697d0cc52f54102bf4 Isabelle94-5
 2cf13a72e1704d0094d21e7dc68e7271a282ed31 Isabelle2008
 33b9b5da3e6faee6ca6969d17e79634d49e5b46a Isabelle94-1
-35fba71ec6ef550178e5f5e44d95d96c6f36eae6 nominal_01
 3e47692e3a3e4c695f6345b3534ed0c36817fd40 Isabelle99-2
 50be659d4222b68f95e9c966097e59091f26acf3 Isabelle99-1
 67692db44c7099ad8789f088003213aeb095e914 Isabelle94-2
@@ -16,11 +15,8 @@
 831a9a7ab9f352c65b0f449630b428304c89362b Isabelle93
 836950047d8508e3c200edc1e07a46c2c5e09cd7 Isabelle94-6
 8d42a7bccf0b0880dff8e46c71c4811be8b2e7ec Isabelle94-7
-a23af144eb47f12354dff090813c796f278e2eb8 nominal_03
 be6b5edbca9ffeb3bace5f4bac5c6478bf8cbdb2 Isabelle98
-cd41a57221d07441647284e239b8d8d77d498ef5 isa94
 ce180e5b7fa056003791fff19cc5cefba193b135 Isabelle2002
-dde117622dace696123b023d1f06cf8d8ef9eb46 nominal_02
 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
diff -r 1f614b4eb367 -r 22ba938ab10f src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Feb 21 16:36:19 2013 +0100
+++ b/src/HOL/ROOT	Thu Feb 21 18:27:28 2013 +0100
@@ -224,7 +224,7 @@
     "Guard/Auth_Guard_Public"
   files "document/root.tex"
 
-session "HOL-UNITY" in UNITY = HOL +
+session "HOL-UNITY" in UNITY = "HOL-Auth" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -232,7 +232,6 @@
     Verifying security protocols using UNITY.
   *}
   options [document_graph]
-  theories [document = false] "../Auth/Public"
   theories
     (*Basic meta-theory*)
     "UNITY_Main"
@@ -276,12 +275,10 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-ZF" in ZF = HOL +
-  description {* *}
   theories MainZF Games
   files "document/root.tex"
 
 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
-  description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
diff -r 1f614b4eb367 -r 22ba938ab10f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Feb 21 16:36:19 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Feb 21 18:27:28 2013 +0100
@@ -718,9 +718,10 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o Proof_Context.theory_of;
 
-        val timing_estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
-        val timing_order = Real.floor (Real.max (Math.log10 (Time.toReal timing_estimate), ~3.0));
-        val pri = Int.min (timing_order - 3, ~1);
+        val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
+        val pri =
+          if estimate = Time.zeroTime then ~1
+	  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
 
         val future_proof = Proof.global_future_proof
           (fn prf =>