# HG changeset patch
# User wenzelm
# Date 1343302531 -7200
# Node ID a69d7dc49f41b0f85ce6ee4195598fa49afa64ea
# Parent  37999ee01156fe3e48ff8215ee8fdfc911185776
tuned;

diff -r 37999ee01156 -r a69d7dc49f41 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 26 12:59:09 2012 +0200
+++ b/src/HOL/ROOT	Thu Jul 26 13:35:31 2012 +0200
@@ -19,7 +19,7 @@
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! (main) in "." = Pure +
+session "HOL-Proofs"! in "." = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
diff -r 37999ee01156 -r a69d7dc49f41 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Thu Jul 26 12:59:09 2012 +0200
+++ b/src/Pure/System/build.ML	Thu Jul 26 13:35:31 2012 +0200
@@ -42,7 +42,7 @@
     (case filter_out (can getenv_strict) condition of
       [] => use_thys options thys
     | conds =>
-        Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
+        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
           " (undefined " ^ commas conds ^ ")\n"))
   end;