merged
authorbulwahn
Mon, 21 Mar 2011 08:29:16 +0100
changeset 42032 143f37194911
parent 42031 2de57cda5b24 (current diff)
parent 42018 878f33040280 (diff)
child 42033 60350051ef93
merged
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/Tools/quickcheck.ML
--- a/NEWS	Fri Mar 18 18:19:42 2011 +0100
+++ b/NEWS	Mon Mar 21 08:29:16 2011 +0100
@@ -50,6 +50,9 @@
   - sledgehammer available_provers ~> sledgehammer supported_provers
     INCOMPATIBILITY.
 
+* "try":
+  - Added "simp:", "intro:", and "elim:" options.
+
 * Function package: discontinued option "tailrec".
 INCOMPATIBILITY. Use partial_function instead.
 
@@ -62,6 +65,9 @@
 
 *** ML ***
 
+* Structure Timing provides various operations for timing; supersedes
+former start_timing/end_timing etc.
+
 * Path.print is the official way to show file-system paths to users
 (including quotes etc.).
 
--- a/doc-src/System/Thy/Presentation.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -448,7 +448,7 @@
     -P PATH      set path for remote theory browsing information
     -Q INT       set threshold for sub-proof parallelization (default 50)
     -T LEVEL     multithreading: trace level (default 0)
-    -V VERSION   declare alternative document VERSION
+    -V VARIANT   declare alternative document VARIANT
     -b           build mode (output heap image, using current dir)
     -d FORMAT    build document as FORMAT (default false)
     -f NAME      use ML file NAME (default ROOT.ML)
@@ -523,16 +523,16 @@
   \secref{sec:tool-latex} for more details.
 
   \medskip The @{verbatim "-V"} option declares alternative document
-  versions, consisting of name/tags pairs (cf.\ options @{verbatim
+  variants, consisting of name/tags pairs (cf.\ options @{verbatim
   "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The
   standard document is equivalent to ``@{verbatim
   "document=theory,proof,ML"}'', which means that all theory begin/end
   commands, proof body texts, and ML code will be presented
-  faithfully.  An alternative version ``@{verbatim
+  faithfully.  An alternative variant ``@{verbatim
   "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
   original text by a short place-holder.  The form ``@{text
   name}@{verbatim "=-"},'' means to remove document @{text name} from
-  the list of versions to be processed.  Any number of @{verbatim
+  the list of variants to be processed.  Any number of @{verbatim
   "-V"} options may be given; later declarations have precedence over
   earlier ones.
 
@@ -682,15 +682,15 @@
   corresponding output files named after @{verbatim root} as well,
   e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
 
-  \medskip When running the session, Isabelle copies the original
-  @{verbatim document} directory into its proper place within
-  @{setting ISABELLE_BROWSER_INFO} according to the session path.
-  Then, for any processed theory @{text A} some {\LaTeX} source is
-  generated and put there as @{text A}@{verbatim ".tex"}.
-  Furthermore, a list of all generated theory files is put into
-  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
-  by the user would include @{verbatim session.tex} to get a document
-  containing all the theories.
+  \medskip When running the session, Isabelle copies the content of
+  the original @{verbatim document} directory into its proper place
+  within @{setting ISABELLE_BROWSER_INFO}, according to the session
+  path and document variant.  Then, for any processed theory @{text A}
+  some {\LaTeX} source is generated and put there as @{text
+  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
+  files is put into @{verbatim session.tex}.  Typically, the root
+  {\LaTeX} file provided by the user would include @{verbatim
+  session.tex} to get a document containing all the theories.
 
   The {\LaTeX} versions of the theories require some macros defined in
   @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
--- a/doc-src/System/Thy/document/Presentation.tex	Fri Mar 18 18:19:42 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex	Mon Mar 21 08:29:16 2011 +0100
@@ -474,7 +474,7 @@
     -P PATH      set path for remote theory browsing information
     -Q INT       set threshold for sub-proof parallelization (default 50)
     -T LEVEL     multithreading: trace level (default 0)
-    -V VERSION   declare alternative document VERSION
+    -V VARIANT   declare alternative document VARIANT
     -b           build mode (output heap image, using current dir)
     -d FORMAT    build document as FORMAT (default false)
     -f NAME      use ML file NAME (default ROOT.ML)
@@ -550,12 +550,12 @@
   \secref{sec:tool-latex} for more details.
 
   \medskip The \verb|-V| option declares alternative document
-  versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
+  variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
   standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
   commands, proof body texts, and ML code will be presented
-  faithfully.  An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
+  faithfully.  An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
   original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
-  the list of versions to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
+  the list of variants to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
   earlier ones.
 
   \medskip The \verb|-g| option produces images of the theory
@@ -693,15 +693,13 @@
   corresponding output files named after \verb|root| as well,
   e.g.\ \verb|root.dvi| for target format \verb|dvi|.
 
-  \medskip When running the session, Isabelle copies the original
-  \verb|document| directory into its proper place within
-  \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} according to the session path.
-  Then, for any processed theory \isa{A} some {\LaTeX} source is
-  generated and put there as \isa{A}\verb|.tex|.
-  Furthermore, a list of all generated theory files is put into
-  \verb|session.tex|.  Typically, the root {\LaTeX} file provided
-  by the user would include \verb|session.tex| to get a document
-  containing all the theories.
+  \medskip When running the session, Isabelle copies the content of
+  the original \verb|document| directory into its proper place
+  within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
+  path and document variant.  Then, for any processed theory \isa{A}
+  some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|.  Furthermore, a list of all generated theory
+  files is put into \verb|session.tex|.  Typically, the root
+  {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.
 
   The {\LaTeX} versions of the theories require some macros defined in
   \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
--- a/lib/Tools/usedir	Fri Mar 18 18:19:42 2011 +0100
+++ b/lib/Tools/usedir	Mon Mar 21 08:29:16 2011 +0100
@@ -21,7 +21,7 @@
   echo "    -P PATH      set path for remote theory browsing information"
   echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
   echo "    -T LEVEL     multithreading: trace level (default 0)"
-  echo "    -V VERSION   declare alternative document VERSION"
+  echo "    -V VARIANT   declare alternative document VARIANT"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
   echo "    -f NAME      use ML file NAME (default ROOT.ML)"
@@ -74,7 +74,7 @@
 MAXTHREADS="1"
 RPATH=""
 TRACETHREADS="0"
-DOCUMENT_VERSIONS=""
+DOCUMENT_VARIANTS=""
 BUILD=""
 DOCUMENT=false
 ROOT_FILE="ROOT.ML"
@@ -122,10 +122,10 @@
         TRACETHREADS="$OPTARG"
         ;;
       V)
-        if [ -z "$DOCUMENT_VERSIONS" ]; then
-          DOCUMENT_VERSIONS="\"$OPTARG\""
+        if [ -z "$DOCUMENT_VARIANTS" ]; then
+          DOCUMENT_VARIANTS="\"$OPTARG\""
         else
-          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
+          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
         fi
         ;;
       b)
@@ -241,7 +241,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
     -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -250,7 +250,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -22,8 +22,7 @@
         "expected file ending " ^ quote ext)
 
     val base_path = Path.explode base_name |> tap check_ext
-    val (full_path, _) =
-      Thy_Load.check_file (Thy_Load.master_directory thy) base_path
+    val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path
 
     val _ = Boogie_VCs.is_closed thy orelse
       error ("Found the beginning of a new Boogie environment, " ^
--- a/src/HOL/Matrix/Compute_Oracle/report.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/report.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -11,9 +11,9 @@
 
 fun timeit f =
     let
-        val t1 = start_timing ()
+        val t1 = Timing.start ()
         val x = f ()
-        val t2 = #message (end_timing t1)
+        val t2 = Timing.message (Timing.result t1)
         val _ = writeln ((report_space ()) ^ "--> "^t2)
     in
         x       
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -210,10 +210,7 @@
   | NONE => default)
 
 fun cpu_time f x =
-  let
-    val start = start_timing ()
-    val result = Exn.capture (fn () => f x) ()
-    val time = Time.toMilliseconds (#cpu (end_timing start))
-  in (Exn.release result, time) end
+  let val ({cpu, ...}, y) = Timing.timing f x
+  in (y, Time.toMilliseconds cpu) end
 
 end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -558,7 +558,7 @@
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial = Try.invoke_try (SOME try_timeout) pre
+      val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
         handle TimeLimit.TimeOut => false
       fun apply_reconstructor m1 m2 =
         if metis_ft
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -150,7 +150,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
-    case Try.invoke_try (SOME (seconds 5.0)) state of
+    case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
       true => (Solved, ([], NONE))
     | false => (Unsolved, ([], NONE))
   end
@@ -332,12 +332,9 @@
 
 fun count x = (length oo filter o equal) x
 
-fun cpu_time description f =
-  let
-    val start = start_timing ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (end_timing start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 (*
 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -15,8 +15,7 @@
 
 fun spark_open vc_name thy =
   let
-    val (vc_path, _) = Thy_Load.check_file
-      (Thy_Load.master_directory thy) (Path.explode vc_name);
+    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
     val (base, header) =
       (case Path.split_ext vc_path of
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
--- a/src/HOL/TLA/Action.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Action.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -12,9 +12,8 @@
 
 (** abstract syntax **)
 
-types
-  'a trfun = "(state * state) => 'a"
-  action   = "bool trfun"
+type_synonym 'a trfun = "(state * state) => 'a"
+type_synonym action   = "bool trfun"
 
 arities prod :: (world, world) world
 
--- a/src/HOL/TLA/Init.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Init.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -14,8 +14,7 @@
 typedecl behavior
 arities behavior :: world
 
-types
-  temporal = "behavior form"
+type_synonym temporal = "behavior form"
 
 
 consts
--- a/src/HOL/TLA/Intensional.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Intensional.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -15,9 +15,8 @@
 
 (** abstract syntax **)
 
-types
-  ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
-  'w form = "('w, bool) expr"
+type_synonym ('w,'a) expr = "'w => 'a"   (* intention: 'w::world, 'a::type *)
+type_synonym 'w form = "('w, bool) expr"
 
 consts
   Valid    :: "('w::world) form => bool"
--- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -8,11 +8,10 @@
 imports Memory RPC MemClerkParameters
 begin
 
-types
-  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
-  mClkSndChType = "memChType"
-  mClkRcvChType = "rpcSndChType"
-  mClkStType    = "(PrIds => mClkState) stfun"
+(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
+type_synonym mClkSndChType = "memChType"
+type_synonym mClkRcvChType = "rpcSndChType"
+type_synonym mClkStType = "(PrIds => mClkState) stfun"
 
 definition
   (* state predicates *)
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -10,11 +10,10 @@
 
 datatype mClkState = clkA | clkB
 
-types
-  (* types sent on the clerk's send and receive channels are argument types
-     of the memory and the RPC, respectively *)
-  mClkSndArgType   = "memOp"
-  mClkRcvArgType   = "rpcOp"
+(* types sent on the clerk's send and receive channels are argument types
+   of the memory and the RPC, respectively *)
+type_synonym mClkSndArgType = "memOp"
+type_synonym mClkRcvArgType = "rpcOp"
 
 definition
   (* translate a memory call to an RPC call *)
--- a/src/HOL/TLA/Memory/Memory.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -8,10 +8,9 @@
 imports MemoryParameters ProcedureInterface
 begin
 
-types
-  memChType  = "(memOp, Vals) channel"
-  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
-  resType = "(PrIds => Vals) stfun"
+type_synonym memChType = "(memOp, Vals) channel"
+type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
+type_synonym resType = "(PrIds => Vals) stfun"
 
 consts
   (* state predicates *)
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -10,8 +10,7 @@
 
 datatype histState = histA | histB
 
-types
-  histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
+type_synonym histType = "(PrIds => histState) stfun"  (* the type of the history variable *)
 
 consts
   (* the specification *)
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -8,15 +8,13 @@
 imports "../TLA" RPCMemoryParams
 begin
 
-typedecl
+typedecl ('a,'r) chan
   (* type of channels with argument type 'a and return type 'r.
      we model a channel as an array of variables (of type chan)
      rather than a single array-valued variable because the
      notation gets a little simpler.
   *)
-  ('a,'r) chan
-types
-  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
+type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
 
 consts
   (* data-level functions *)
--- a/src/HOL/TLA/Memory/RPC.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -8,10 +8,9 @@
 imports RPCParameters ProcedureInterface Memory
 begin
 
-types
-  rpcSndChType  = "(rpcOp,Vals) channel"
-  rpcRcvChType  = "memChType"
-  rpcStType     = "(PrIds => rpcState) stfun"
+type_synonym rpcSndChType = "(rpcOp,Vals) channel"
+type_synonym rpcRcvChType = "memChType"
+type_synonym rpcStType = "(PrIds => rpcState) stfun"
 
 consts
   (* state predicates *)
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -8,10 +8,10 @@
 imports Main
 begin
 
-types
-  bit = "bool"   (* Signal wires for the procedure interface.
-                    Defined as bool for simplicity. All I should really need is
-                    the existence of two distinct values. *)
+type_synonym bit = "bool"
+ (* Signal wires for the procedure interface.
+    Defined as bool for simplicity. All I should really need is
+    the existence of two distinct values. *)
 
 (* all of these are simple (HOL) types *)
 typedecl Locs    (* "syntactic" value type *)
--- a/src/HOL/TLA/Stfun.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/TLA/Stfun.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -13,9 +13,8 @@
 
 arities state :: world
 
-types
-  'a stfun = "state => 'a"
-  stpred  = "bool stfun"
+type_synonym 'a stfun = "state => 'a"
+type_synonym stpred  = "bool stfun"
 
 
 consts
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -300,6 +300,24 @@
   | bound_for_plain_rel _ _ u =
     raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
 
+fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
+  case constrs of
+    [_, _] =>
+    (case constrs |> map (snd o #const) |> List.partition is_fun_type of
+       ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
+     | _ => false)
+  | _ => false
+
+fun needed_values need_vals T =
+  AList.lookup (op =) need_vals T |> the_default NONE |> these
+
+fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) =
+  length (needed_values need_vals typ) = card
+
+fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) =
+    exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us
+  | is_sel_of_constr _ _ = false
+
 fun bound_for_sel_rel ctxt debug need_vals dtypes
         (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
                   R as Func (Atom (_, j0), R2), nick)) =
@@ -308,46 +326,80 @@
       val {delta, epsilon, exclusive, explicit_max, ...} =
         constr_spec dtypes (constr_s, T1)
       val dtype as {card, ...} = datatype_spec dtypes T1 |> the
-      val need_vals =
-        AList.lookup (op =) need_vals T1 |> the_default NONE |> these
+      val T1_need_vals = needed_values need_vals T1
     in
       ([(x, bound_comment ctxt debug nick T R)],
        let
-         val complete_need_vals = (length need_vals = card)
+         val discr = (R2 = Formula Neut)
+         val complete_need_vals = (length T1_need_vals = card)
          val (my_need_vals, other_need_vals) =
-           need_vals
-           |> List.partition
-                  (fn (Construct (sel_us, _, _, _), _) =>
-                      exists (fn FreeRel (x', _, _, _) => x = x'
-                               | _ => false) sel_us
-                    | _ => false)
-         fun upper_bound_ts () =
-           if complete_need_vals then
-             my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet
-           else if not (null other_need_vals) then
-             index_seq (delta + j0) (epsilon - delta)
-             |> filter_out (member (op = o apsnd snd) other_need_vals)
-             |> map (KK.Tuple o single) |> KK.TupleSet
+           T1_need_vals |> List.partition (is_sel_of_constr x)
+         fun atom_seq_for_self_rec j =
+           if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0)
+         fun exact_bound_for_perhaps_needy_atom j =
+           case AList.find (op =) my_need_vals j of
+             [constr_u] =>
+             let
+               val n = sel_no_from_name nick
+               val arg_u =
+                 case constr_u of
+                   Construct (_, _, _, arg_us) => nth arg_us n
+                 | _ => raise Fail "expected \"Construct\""
+               val T2_need_vals = needed_values need_vals T2
+             in
+               case AList.lookup (op =) T2_need_vals arg_u of
+                 SOME arg_j => SOME (KK.TupleAtomSeq (1, arg_j))
+               | _ => NONE
+             end
+           | _ => NONE
+         fun n_fold_tuple_union [] = KK.TupleSet []
+           | n_fold_tuple_union (ts :: tss) =
+             fold (curry (KK.TupleUnion o swap)) tss ts
+         fun tuple_perhaps_needy_atom upper j =
+           single_atom j
+           |> not discr
+              ? (fn ts => KK.TupleProduct (ts,
+                              case exact_bound_for_perhaps_needy_atom j of
+                                SOME ts => ts
+                              | NONE => if upper then upper_bound_for_rep R2
+                                        else KK.TupleSet []))
+         fun bound_tuples upper =
+           if null T1_need_vals then
+             if upper then
+               KK.TupleAtomSeq (epsilon - delta, delta + j0)
+               |> not discr
+                  ? (fn ts => KK.TupleProduct (ts, upper_bound_for_rep R2))
+             else
+               KK.TupleSet []
            else
-             KK.TupleAtomSeq (epsilon - delta, delta + j0)
+             (if complete_need_vals then
+                my_need_vals |> map snd
+              else
+                index_seq (delta + j0) (epsilon - delta)
+                |> filter_out (member (op = o apsnd snd) other_need_vals))
+             |> map (tuple_perhaps_needy_atom upper)
+             |> n_fold_tuple_union
        in
          if explicit_max = 0 orelse
-            (complete_need_vals andalso null my_need_vals) (* ### needed? *) then
+            (complete_need_vals andalso null my_need_vals) then
            [KK.TupleSet []]
          else
-           if R2 = Formula Neut then
-             [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet [])
+           if discr then
+             [bound_tuples true]
+             |> not (exclusive orelse all_values_are_needed need_vals dtype)
+                ? cons (KK.TupleSet [])
            else
-             [KK.TupleSet [],
+             [bound_tuples false,
               if T1 = T2 andalso epsilon > delta andalso
                  is_datatype_acyclic dtype then
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
                            KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
-                                            KK.TupleAtomSeq (j, j0)))
-                |> foldl1 KK.TupleUnion
+                               KK.TupleAtomSeq (atom_seq_for_self_rec j)))
+                |> n_fold_tuple_union
               else
-                KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)]
+                bound_tuples true]
+             |> distinct (op =)
          end)
     end
   | bound_for_sel_rel _ _ _ _ u =
@@ -1499,14 +1551,14 @@
   let val dummy_u = RelReg (0, type_of u, rep_of u) in
     case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u)
          |> kodkod_formula_from_nut ofs kk of
-      KK.RelEq (KK.RelReg _, r) => KK.RelEq (KK.Atom j, r)
+      KK.RelEq (KK.RelReg _, r) => SOME (KK.RelEq (KK.Atom j, r))
     | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut",
                       "malformed Kodkod formula")
   end
 
 fun needed_values_for_datatype [] _ _ = SOME []
   | needed_values_for_datatype need_us ofs
-        ({typ, card, constrs, ...} : datatype_spec) =
+                               ({typ, card, constrs, ...} : datatype_spec) =
     let
       fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
           fold aux us
@@ -1537,9 +1589,10 @@
       SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
     end
 
-fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]
-  | needed_value_axioms_for_datatype ofs kk (SOME fixed) =
-    fixed |> map (atom_equation_for_nut ofs kk)
+fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False]
+  | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) =
+    if is_datatype_nat_like (the (datatype_spec dtypes T)) then []
+    else fixed |> map_filter (atom_equation_for_nut ofs kk)
 
 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
   kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
@@ -1707,27 +1760,35 @@
            |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
                                                   nfas dtypes)
 
-fun sel_axiom_for_sel hol_ctxt binarize j0
+fun sel_axioms_for_sel hol_ctxt binarize j0
         (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
-        rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
-        n =
+        need_vals rel_table dom_r (dtype as {typ, ...})
+        ({const, delta, epsilon, exclusive, ...} : constr_spec) n =
   let
     val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
     val (r, R, _) = const_triple rel_table x
+    val rel_x =
+      case r of
+        KK.Rel x => x
+      | _ => raise BAD ("Nitpick_Kodkod.sel_axioms_for_sel", "non-Rel")
     val R2 = dest_Func R |> snd
     val z = (epsilon - delta, delta + j0)
   in
     if exclusive then
-      kk_n_ary_function kk (Func (Atom z, R2)) r
+      [kk_n_ary_function kk (Func (Atom z, R2)) r]
+    else if all_values_are_needed need_vals dtype then
+      typ |> needed_values need_vals
+          |> filter (is_sel_of_constr rel_x)
+          |> map (fn (_, j) => kk_n_ary_function kk R2 (kk_join (KK.Atom j) r))
     else
       let val r' = kk_join (KK.Var (1, 0)) r in
-        kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
-               (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
-                              (kk_n_ary_function kk R2 r') (kk_no r'))
+        [kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
+                (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
+                               (kk_n_ary_function kk R2 r') (kk_no r'))]
       end
   end
-fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
-        (constr as {const, delta, epsilon, explicit_max, ...}) =
+fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table
+        dtype (constr as {const, delta, epsilon, explicit_max, ...}) =
   let
     val honors_explicit_max =
       explicit_max < 0 orelse epsilon - delta <= explicit_max
@@ -1749,17 +1810,20 @@
                              " too small for \"max\"")
       in
         max_axiom ::
-        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
-            (index_seq 0 (num_sels_for_constr_type (snd const)))
+        maps (sel_axioms_for_sel hol_ctxt binarize j0 kk need_vals rel_table
+                                 dom_r dtype constr)
+             (index_seq 0 (num_sels_for_constr_type (snd const)))
       end
   end
-fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
-                            ({constrs, ...} : datatype_spec) =
-  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
+                            (dtype as {constrs, ...}) =
+  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
+                              dtype) constrs
 
-fun uniqueness_axiom_for_constr hol_ctxt binarize
+fun uniqueness_axioms_for_constr hol_ctxt binarize
         ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
-         : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
+         : kodkod_constrs) need_vals rel_table dtype
+        ({const, ...} : constr_spec) =
   let
     fun conjunct_for_sel r =
       kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
@@ -1771,36 +1835,42 @@
     val set_r = triples |> hd |> #1
   in
     if num_sels = 0 then
-      kk_lone set_r
+      [kk_lone set_r]
+    else if all_values_are_needed need_vals dtype then
+      []
     else
-      kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
-             (kk_implies
-                  (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
-                  (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
+      [kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
+              (kk_implies
+                   (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
+                   (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
   end
-fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
-                                   ({constrs, ...} : datatype_spec) =
-  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
+                                   (dtype as {constrs, ...}) =
+  maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
+                                     dtype) constrs
 
 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
 fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
-                                  rel_table
-                                  ({card, constrs, ...} : datatype_spec) =
+        need_vals rel_table (dtype as {card, constrs, ...}) =
   if forall #exclusive constrs then
     [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
+  else if all_values_are_needed need_vals dtype then
+    []
   else
     let val rs = map (discr_rel_expr rel_table o #const) constrs in
       [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
        kk_disjoint_sets kk rs]
     end
 
-fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
-  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
+fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = []
+  | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table
                               (dtype as {typ, ...}) =
     let val j0 = offset_of_type ofs typ in
-      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
-      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
-      partition_axioms_for_datatype j0 kk rel_table dtype
+      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table
+                              dtype @
+      uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
+                                     dtype @
+      partition_axioms_for_datatype j0 kk need_vals rel_table dtype
     end
 
 fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
@@ -1812,11 +1882,11 @@
              |> strongly_connected_sub_nfas
   in
     acyclicity_axioms_for_datatypes kk nfas @
-    maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @
+    maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @
     sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
                                    kk rel_table nfas dtypes @
-    maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
-         dtypes
+    maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk
+                                    rel_table) dtypes
   end
 
 end;
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -527,10 +527,10 @@
     val rs = these (AList.lookup (op =) clauses p)
     fun check_mode m =
       let
-        val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
+        val res = cond_timeit false "work part of check_mode for one mode" (fn _ => 
           map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
       in
-        Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
+        cond_timeit false "aux part of check_mode for one mode" (fn _ => 
         case find_indices is_none res of
           [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
         | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
@@ -538,7 +538,7 @@
     val _ = if show_mode_inference options then
         tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
       else ()
-    val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
+    val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
     val (ms', errors) = split res
   in
     ((p, (ms' : ((bool * mode) * bool) list)), errors)
@@ -622,7 +622,7 @@
       (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
         (modes @ extra_modes)) modes
     val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
-      Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
+      cond_timeit false "Fixpount computation of mode analysis" (fn () =>
       if show_invalid_clauses options then
         fixp_with_state (fn (modes, errors) =>
           let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -130,12 +130,12 @@
 fun preprocess options t thy =
   let
     val _ = print_step options "Fetching definitions from theory..."
-    val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
+    val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
           (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
           |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
     val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   in
-    Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
+    cond_timeit (!Quickcheck.timing) "preprocess-process"
       (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
         (Term_Graph.strong_conn gr) thy))
   end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -1363,7 +1363,7 @@
     val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
       modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
     val ((moded_clauses, needs_random), errors) =
-      Output.cond_timeit (!Quickcheck.timing) "Infering modes"
+      cond_timeit (!Quickcheck.timing) "Infering modes"
       (fn _ => infer_modes mode_analysis_options
         options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
     val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
@@ -1373,19 +1373,19 @@
     val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =
-      Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
+      cond_timeit (!Quickcheck.timing) "Defining executable functions..."
       (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
       |> Theory.checkpoint)
     val ctxt'' = ProofContext.init_global thy''
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
-      Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
+      cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
         compile_preds options
           (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
     val _ = print_compiled_terms options ctxt'' compiled_terms
     val _ = print_step options "Proving equations..."
     val result_thms =
-      Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
+      cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
       #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
     val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
       (maps_modes result_thms)
@@ -1393,7 +1393,7 @@
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
       (fn thm => Context.mapping (Code.add_eqn thm) I))))
     val thy''' =
-      Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
+      cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
       fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib thy ])] thy))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -211,12 +211,9 @@
 
 val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
-fun cpu_time description f =
-  let
-    val start = start_timing ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (end_timing start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 
 fun compile_term compilation options ctxt (t, eval_terms) =
   let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -115,8 +115,8 @@
   let
     val ths = Attrib.eval_thms ctxt [xthm]
     val bracket =
-      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
-                               ^ "]") args)
+      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
+      |> implode
     fun nth_name j =
       case xref of
         Facts.Fact s => backquote s ^ bracket
--- a/src/HOL/Tools/try.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/try.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -7,7 +7,9 @@
 signature TRY =
 sig
   val auto : bool Unsynchronized.ref
-  val invoke_try : Time.time option -> Proof.state -> bool
+  val invoke_try :
+    Time.time option -> string list * string list * string list -> Proof.state
+    -> bool
   val setup : theory -> theory
 end;
 
@@ -40,59 +42,85 @@
       NONE
   end
 
-fun named_method thy name =
-  Method.method thy (Args.src ((name, []), Position.none))
+val parse_method =
+  enclose "(" ")"
+  #> Outer_Syntax.scan Position.start
+  #> filter Token.is_proper
+  #> Scan.read Token.stopper Method.parse
+  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
 
-fun apply_named_method_on_first_goal name ctxt =
-  let val thy = ProofContext.theory_of ctxt in
-    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
-  end
+fun apply_named_method_on_first_goal method thy =
+  method |> parse_method
+         |> Method.method thy
+         |> Method.Basic
+         |> curry Method.SelectGoals 1
+         |> Proof.refine
   handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
 
-fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
+fun add_attr_text (NONE, _) s = s
+  | add_attr_text (_, []) s = s
+  | add_attr_text (SOME x, fs) s =
+    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
+fun attrs_text (sx, ix, ex) (ss, is, es) =
+  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
+
+fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
+                    triple st =
   if not auto orelse run_if_auto then
-    do_generic timeout_opt
-               (name ^ (if all_goals andalso
-                           nprems_of (#goal (Proof.goal st)) > 1 then
-                          "[1]"
-                        else
-                          "")) I (#goal o Proof.goal)
-               (apply_named_method_on_first_goal name (Proof.context_of st)) st
+    let val attrs = attrs_text attrs triple in
+      do_generic timeout_opt
+                 (name ^ (if all_goals andalso
+                             nprems_of (#goal (Proof.goal st)) > 1 then
+                            "[1]"
+                          else
+                            "") ^
+                  attrs) I (#goal o Proof.goal)
+                 (apply_named_method_on_first_goal (name ^ attrs)
+                                                   (Proof.theory_of st)) st
+    end
   else
     NONE
 
-(* name * (all_goals, run_if_auto) *)
+val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
+val clas_attrs = (NONE, SOME "intro", SOME "elim")
+val simp_attrs = (SOME "add", NONE, NONE)
+val metis_attrs = (SOME "", SOME "", SOME "")
+val no_attrs = (NONE, NONE, NONE)
+
+(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
 val named_methods =
-  [("simp", (false, true)),
-   ("auto", (true, true)),
-   ("fast", (false, false)),
-   ("fastsimp", (false, false)),
-   ("force", (false, false)),
-   ("blast", (false, true)),
-   ("metis", (false, true)),
-   ("linarith", (false, true)),
-   ("presburger", (false, true))]
+  [("simp", ((false, true), simp_attrs)),
+   ("auto", ((true, true), full_attrs)),
+   ("fast", ((false, false), clas_attrs)),
+   ("fastsimp", ((false, false), full_attrs)),
+   ("force", ((false, false), full_attrs)),
+   ("blast", ((false, true), clas_attrs)),
+   ("metis", ((false, true), metis_attrs)),
+   ("linarith", ((false, true), no_attrs)),
+   ("presburger", ((false, true), no_attrs))]
 val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
 
-fun do_try auto timeout_opt st =
+fun do_try auto timeout_opt triple st =
   let
     val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
   in
-    case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
+    case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
                     |> map_filter I |> sort (int_ord o pairself snd) of
       [] => (if auto then () else writeln "No proof found."; (false, st))
     | xs as (s, _) :: _ =>
       let
-        val xs = xs |> map swap |> AList.coalesce (op =)
+        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
+                    |> AList.coalesce (op =)
                     |> map (swap o apsnd commas)
+        val need_parens = exists_string (curry (op =) " ") s
         val message =
           (if auto then "Auto Try found a proof" else "Try this command") ^
           ": " ^
           Markup.markup Markup.sendback
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
-                else "apply") ^ " " ^ s) ^
+                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
       in
         (true, st |> (if auto then
@@ -105,17 +133,43 @@
       end
   end
 
-val invoke_try = fst oo do_try false
+fun invoke_try timeout_opt = fst oo do_try false timeout_opt
 
 val tryN = "try"
 
+fun try_trans triple =
+  Toplevel.keep (K () o do_try false (SOME default_timeout) triple
+                 o Toplevel.proof_of)
+
+fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
+
+fun string_of_xthm (xref, args) =
+  Facts.string_of_ref xref ^
+  implode (map (enclose "[" "]" o Pretty.str_of
+                o Args.pretty_src @{context}) args)
+
+val parse_fact_refs =
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+                            (Parse_Spec.xthm >> string_of_xthm))
+val parse_attr =
+     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
+     >> (fn ss => (ss, [], []))
+  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
+     >> (fn is => ([], is, []))
+  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
+     >> (fn es => ([], [], es))
+fun parse_attrs x =
+    (Args.parens parse_attrs
+  || Scan.repeat parse_attr
+     >> (fn triple => fold merge_attrs triple ([], [], []))) x
+
+val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
+
 val _ =
   Outer_Syntax.improper_command tryN
-      "try a combination of proof methods" Keyword.diag
-      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
-                                    o Toplevel.proof_of)))
+      "try a combination of proof methods" Keyword.diag parse_try_command
 
-val auto_try = do_try true NONE
+val auto_try = do_try true NONE ([], [], [])
 
 val setup = Auto_Tools.register_tool (auto, auto_try)
 
--- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Mon Mar 21 08:29:16 2011 +0100
@@ -536,13 +536,12 @@
   fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
     | and_to_list fm acc = rev (fm :: acc)
   val clauses = and_to_list prop_fm []
-  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
-    clauses
-  val cterms  = map (Thm.cterm_of @{theory}) terms
-  val timer   = start_timing ()
-  val thm     = sat.rawsat_thm @{context} cterms
+  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
+  val cterms = map (Thm.cterm_of @{theory}) terms
+  val start = Timing.start ()
+  val thm = sat.rawsat_thm @{context} cterms
 in
-  (end_timing timer, !sat.counter)
+  (Timing.result start, ! sat.counter)
 end;
 *}
 
--- a/src/Provers/blast.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Provers/blast.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -914,7 +914,7 @@
 
 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
   if b then
-    writeln (#message (end_timing start) ^ " for search.  Closed: "
+    writeln (Timing.message (Timing.result start) ^ " for search.  Closed: "
              ^ string_of_int (!nclosed) ^
              " tried: " ^ string_of_int (!ntried) ^
              " tactics: " ^ string_of_int (length tacs))
@@ -1256,7 +1256,7 @@
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
       fun cont (tacs,_,choices) =
-          let val start = start_timing ()
+          let val start = Timing.start ()
           in
           case Seq.pull(EVERY' (rev tacs) i st) of
               NONE => (writeln ("PROOF FAILED for depth " ^
@@ -1265,7 +1265,7 @@
                        else ();
                        backtrack choices)
             | cell => (if (!trace orelse !stats)
-                       then writeln (#message (end_timing start) ^ " for reconstruction")
+                       then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
                        else ();
                        Seq.make(fn()=> cell))
           end
@@ -1273,13 +1273,13 @@
   handle PROVE     => Seq.empty
 
 (*Public version with fixed depth*)
-fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
+fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
 
 val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
 
 fun blast_tac cs i st =
     ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
-        (timing_depth_tac (start_timing ()) cs) 0) i
+        (timing_depth_tac (Timing.start ()) cs) 0) i
      THEN flexflex_tac) st
     handle TRANS s =>
       ((if !trace then warning ("blast: " ^ s) else ());
@@ -1299,7 +1299,7 @@
   let
     val state as State {fullTrace = ft, ...} = initialize thy;
     val res = timeap prove
-      (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
+      (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
     val _ = fullTrace := !ft;
   in res end;
 
--- a/src/Pure/General/file.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/General/file.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -11,12 +11,13 @@
   val shell_path: Path.T -> string
   val cd: Path.T -> unit
   val pwd: unit -> Path.T
-  val full_path: Path.T -> Path.T
+  val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
-  val check: Path.T -> unit
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool
+  val check_dir: Path.T -> Path.T
+  val check_file: Path.T -> Path.T
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -51,9 +52,18 @@
 val cd = cd o platform_path;
 val pwd = Path.explode o pwd;
 
-fun full_path path =
-  if Path.is_absolute path then path
-  else Path.append (pwd ()) path;
+
+(* full_path *)
+
+fun full_path dir path =
+  let
+    val path' = Path.expand path;
+    val _ = Path.is_current path' andalso error "Bad file specification";
+    val path'' = Path.append dir path';
+  in
+    if Path.is_absolute path'' then path''
+    else Path.append (pwd ()) path''
+  end;
 
 
 (* tmp_path *)
@@ -66,15 +76,19 @@
 
 val exists = can OS.FileSys.modTime o platform_path;
 
-fun check path =
-  if exists path then ()
-  else error ("No such file or directory: " ^ Path.print path);
-
 val rm = OS.FileSys.remove o platform_path;
 
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));
 
+fun check_dir path =
+  if exists path andalso is_dir path then path
+  else error ("No such directory: " ^ Path.print path);
+
+fun check_file path =
+  if exists path andalso not (is_dir path) then path
+  else error ("No such file: " ^ Path.print path);
+
 
 (* open files *)
 
--- a/src/Pure/General/markup.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/General/markup.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -100,7 +100,7 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
-  val timingN: string val timing: timing -> T
+  val timingN: string val timing: Timing.timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
@@ -312,7 +312,7 @@
 val cpuN = "cpu";
 val gcN = "gc";
 
-fun timing ({elapsed, cpu, gc, ...}: timing) =
+fun timing {elapsed, cpu, gc} =
   (timingN,
    [(elapsedN, Time.toString elapsed),
     (cpuN, Time.toString cpu),
--- a/src/Pure/General/output.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/General/output.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/output.ML
     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
 
-Output channels and timing messages.
+Isabelle output channels.
 *)
 
 signature BASIC_OUTPUT =
@@ -10,11 +10,6 @@
   val tracing: string -> unit
   val warning: string -> unit
   val legacy_feature: string -> unit
-  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
-  val timeit: (unit -> 'a) -> 'a
-  val timeap: ('a -> 'b) -> 'a -> 'b
-  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
-  val timing: bool Unsynchronized.ref
 end;
 
 signature OUTPUT =
@@ -111,31 +106,6 @@
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
-
-
-(** timing **)
-
-(*conditional timing with message*)
-fun cond_timeit flag msg e =
-  if flag then
-    let
-      val start = start_timing ();
-      val result = Exn.capture e ();
-      val end_msg = #message (end_timing start);
-      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
-    in Exn.release result end
-  else e ();
-
-(*unconditional timing*)
-fun timeit e = cond_timeit true "" e;
-
-(*timed application function*)
-fun timeap f x = timeit (fn () => f x);
-fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-
-(*global timing mode*)
-val timing = Unsynchronized.ref false;
-
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;
--- a/src/Pure/General/timing.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/General/timing.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -4,19 +4,46 @@
 Basic support for time measurement.
 *)
 
-val seconds = Time.fromReal;
+signature BASIC_TIMING =
+sig
+  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
+  val timeit: (unit -> 'a) -> 'a
+  val timeap: ('a -> 'b) -> 'a -> 'b
+  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
+end
 
-fun start_timing () =
+signature TIMING =
+sig
+  include BASIC_TIMING
+  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+  type start
+  val start: unit -> start
+  val result: start -> timing
+  val timing: ('a -> 'b) -> 'a -> timing * 'b
+  val message: timing -> string
+end
+
+structure Timing: TIMING =
+struct
+
+(* timer control *)
+
+type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
+
+abstype start = Start of
+  Timer.real_timer * Time.time * Timer.cpu_timer *
+    {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
+with
+
+fun start () =
   let
     val real_timer = Timer.startRealTimer ();
     val real_time = Timer.checkRealTimer real_timer;
     val cpu_timer = Timer.startCPUTimer ();
     val cpu_times = Timer.checkCPUTimes cpu_timer;
-  in (real_timer, real_time, cpu_timer, cpu_times) end;
+  in Start (real_timer, real_time, cpu_timer, cpu_times) end;
 
-type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
-
-fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
+fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
   let
     val real_time2 = Timer.checkRealTimer real_timer;
     val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
@@ -27,10 +54,41 @@
     val elapsed = real_time2 - real_time;
     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
     val cpu = usr2 - usr + sys2 - sys + gc;
+  in {elapsed = elapsed, cpu = cpu, gc = gc} end;
 
-    val message =
-     (toString elapsed ^ "s elapsed time, " ^
-      toString cpu ^ "s cpu time, " ^
-      toString gc ^ "s GC time") handle Time.Time => "";
-  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+end;
+
+fun timing f x =
+  let
+    val start = start ();
+    val y = f x;
+  in (result start, y) end;
+
+
+(* timing messages *)
+
+fun message {elapsed, cpu, gc} =
+  Time.toString elapsed ^ "s elapsed time, " ^
+  Time.toString cpu ^ "s cpu time, " ^
+  Time.toString gc ^ "s GC time" handle Time.Time => "";
 
+fun cond_timeit enabled msg e =
+  if enabled then
+    let
+      val (timing, result) = timing (Exn.capture e) ();
+      val end_msg = message timing;
+      val _ =
+        if Exn.is_interrupt_exn result then ()
+        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+    in Exn.release result end
+  else e ();
+
+fun timeit e = cond_timeit true "" e;
+fun timeap f x = timeit (fn () => f x);
+fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
+
+end;
+
+structure Basic_Timing: BASIC_TIMING = Timing;
+open Basic_Timing;
+
--- a/src/Pure/IsaMakefile	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/IsaMakefile	Mon Mar 21 08:29:16 2011 +0100
@@ -21,7 +21,6 @@
 
 BOOTSTRAP_FILES = 					\
   General/exn.ML					\
-  General/timing.ML					\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
   ML-Systems/ml_name_space.ML				\
@@ -101,6 +100,7 @@
   General/symbol.ML					\
   General/symbol_pos.ML					\
   General/table.ML					\
+  General/timing.ML					\
   General/url.ML					\
   General/xml.ML					\
   General/xml_data.ML					\
--- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -271,7 +271,7 @@
 fun load_thy name init pos text =
   let
     val (lexs, commands) = get_syntax ();
-    val time = ! Output.timing;
+    val time = ! Toplevel.timing;
 
     val _ = Present.init_theory name;
 
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -218,7 +218,7 @@
 val quiet = Unsynchronized.ref false;
 val debug = Runtime.debug;
 val interact = Unsynchronized.ref false;
-val timing = Output.timing;
+val timing = Unsynchronized.ref false;
 val profiling = Unsynchronized.ref 0;
 val skip_proofs = Unsynchronized.ref false;
 
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -14,10 +14,12 @@
 else use "ML-Systems/single_assignment_polyml.ML";
 
 use "ML-Systems/multithreading.ML";
-use "General/timing.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
 
+val seconds = Time.fromReal;
+
+
 
 (** ML system and platform related **)
 
--- a/src/Pure/ML-Systems/proper_int.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -13,8 +13,6 @@
 
 (* Int *)
 
-structure OrigInt = Int;
-structure OrigIntInf = IntInf;
 type int = IntInf.int;
 
 structure IntInf =
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -13,7 +13,6 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
-use "General/timing.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
 structure PolyML = struct end;
@@ -21,8 +20,9 @@
 use "ML-Systems/use_context.ML";
 
 
+val seconds = Time.fromReal;
+
 (*low-level pointer equality*)
-
 CM.autoload "$smlnj/init/init.cmi";
 val pointer_eq = InlineT.ptreql;
 
--- a/src/Pure/PIDE/document.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -241,9 +241,9 @@
         val is_proof = Keyword.is_proof (Toplevel.name_of tr);
         val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
 
-        val start = start_timing ();
+        val start = Timing.start ();
         val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
-        val _ = timing tr (end_timing start);
+        val _ = timing tr (Timing.result start);
         val _ = List.app (Toplevel.error_msg tr) errs;
         val res =
           (case result of
--- a/src/Pure/ProofGeneral/pgip_types.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -364,7 +364,9 @@
 
 fun string_of_pgipurl p = Path.implode p
 
-fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl)))
+fun attrval_of_pgipurl purl =
+  "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl))
+
 fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)]
 
 val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"
--- a/src/Pure/ProofGeneral/preferences.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -156,7 +156,7 @@
   bool_pref Pattern.trace_unify_fail
     "trace-unification"
     "Output error diagnostics during unification",
-  bool_pref Output.timing
+  bool_pref Toplevel.timing
     "global-timing"
     "Whether to enable timing in Isabelle.",
   bool_pref Toplevel.debug
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -588,14 +588,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
+                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
+            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
--- a/src/Pure/ROOT.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/ROOT.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -21,6 +21,7 @@
 use "General/alist.ML";
 use "General/table.ML";
 use "General/output.ML";
+use "General/timing.ML";
 use "General/properties.ML";
 use "General/markup.ML";
 use "General/scan.ML";
--- a/src/Pure/System/session.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/System/session.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -92,22 +92,21 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
-fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+fun use_dir item root build modes reset info doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
      (init reset parent name;
-      Present.init build info doc doc_graph doc_versions (path ()) name
+      Present.init build info doc doc_graph doc_variants (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
       if timing then
         let
-          val start = start_timing ();
+          val start = Timing.start ();
           val _ = use root;
-          val stop = end_timing start;
           val _ =
             Output.raw_stderr ("Timing " ^ item ^ " (" ^
               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
-              #message stop ^ ")\n");
+              Timing.message (Timing.result start) ^ ")\n");
         in () end
       else use root;
       finish ()))
--- a/src/Pure/Thy/present.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Thy/present.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -6,7 +6,7 @@
 
 signature BASIC_PRESENT =
 sig
-  val no_document: ('a -> 'b) -> 'a -> 'b
+  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
 end;
 
 signature PRESENT =
@@ -18,8 +18,9 @@
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
   val init: bool -> bool -> string -> bool -> string list -> string list ->
-    string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit
-  val finish: unit -> unit
+    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
+    theory list -> unit  (*not thread-safe!*)
+  val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
   val theory_source: string -> (unit -> HTML.text) -> unit
   val theory_output: string -> string -> unit
@@ -64,7 +65,7 @@
 
 (** additional theory data **)
 
-structure BrowserInfoData = Theory_Data
+structure Browser_Info = Theory_Data
 (
   type T = {name: string, session: string list, is_local: bool};
   val empty = {name = "", session = [], is_local = false}: T;
@@ -72,8 +73,8 @@
   fun merge _ = empty;
 );
 
-val put_info = BrowserInfoData.put;
-val get_info = BrowserInfoData.get;
+val put_info = Browser_Info.put;
+val get_info = Browser_Info.get;
 val session_name = #name o get_info;
 
 
@@ -107,7 +108,6 @@
   let
     val name = Context.theory_name thy;
     val {name = sess_name, session, is_local} = get_info thy;
-    val path' = Path.append (Path.make session) (html_path name);
     val entry =
      {name = name, ID = ID_of session name, dir = sess_name,
       path =
@@ -165,14 +165,14 @@
   CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
 
 val suppress_tex_source = Unsynchronized.ref false;
-fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;  (* FIXME unreliable *)
+fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
 
 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
     (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
 
 fun change_theory_info name f =
-  change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
+  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
     (case Symtab.lookup theories name of
       NONE => error ("Browser info: cannot access theory document " ^ quote name)
     | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
@@ -203,9 +203,6 @@
 fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   (tex_source, Buffer.add txt html_source, html));
 
-fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
-  (tex_source, html_source, Buffer.add txt html));
-
 
 
 (** global session state **)
@@ -215,16 +212,16 @@
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
     info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
-    doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option,
-    remote_path: Url.T option, verbose: bool, readme: Path.T option};
+    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
+    readme: Path.T option};
 
 fun make_session_info
   (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
-    doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
+    dump_prefix, remote_path, verbose, readme) =
   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
     info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
-    doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
-    verbose = verbose, readme = readme}: session_info;
+    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
+    readme = readme}: session_info;
 
 
 (* state *)
@@ -232,7 +229,6 @@
 val session_info = Unsynchronized.ref (NONE: session_info option);
 
 fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
-fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
 
 
 
@@ -256,22 +252,22 @@
     session_entries (get_entries dir) ^ HTML.end_document
   |> File.write (Path.append dir index_path);
 
-fun update_index dir name = CRITICAL (fn () =>
+fun update_index dir name =
   (case try get_entries dir of
     NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
-  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
+  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
 
 
-(* document versions *)
+(* document variants *)
 
-fun read_version str =
+fun read_variant str =
   (case space_explode "=" str of
     [name] => (name, "")
   | [name, tags] => (name, tags)
-  | _ => error ("Malformed document version specification: " ^ quote str));
+  | _ => error ("Malformed document variant specification: " ^ quote str));
 
-fun read_versions strs =
-  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
+fun read_variants strs =
+  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
 
 
@@ -279,9 +275,9 @@
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info doc doc_graph doc_versions path name doc_prefix2
-    (remote_path, first_time) verbose thys = CRITICAL (fn () =>
-  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
+fun init build info doc doc_graph doc_variants path name dump_prefix
+    (remote_path, first_time) verbose thys =
+  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
@@ -290,16 +286,15 @@
       val sess_prefix = Path.make path;
       val html_prefix = Path.append (Path.expand output_path) sess_prefix;
 
-      val (doc_prefix1, documents) =
-        if doc = "" then (NONE, [])
-        else if not (File.exists document_path) then
-          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
-            (NONE, []))
-        else (SOME (Path.append html_prefix document_path, html_prefix),
-          read_versions doc_versions);
+      val documents =
+        if doc = "" then []
+        else if not (can File.check_dir document_path) then
+          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
+        else read_variants doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
-      val index_up_lnk = if first_time then
+      val index_up_lnk =
+        if first_time then
           Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
         else Url.File parent_index_path;
       val readme =
@@ -309,15 +304,16 @@
 
       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
-        map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
+          map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
         (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
-      session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
-      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
+      session_info :=
+        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
+          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index (0, index_text)
-    end);
+    end;
 
 
 (* isabelle tool wrappers *)
@@ -365,9 +361,9 @@
   write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
 
 
-fun finish () = CRITICAL (fn () =>
-    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
-      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
+fun finish () =
+  with_session () (fn {name, info, html_prefix, doc_format,
+    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
@@ -379,7 +375,7 @@
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
-      if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
+      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
         SOME (isabelle_browser sorted_graph)
       else NONE;
 
@@ -393,41 +389,46 @@
           File.write (Path.append path graph_eps_path) eps));
       write_tex_index tex_index path;
       List.app (finish_tex path) thys);
+    val _ =
+      if info then
+       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
+        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
+        File.write (Path.append html_prefix session_entries_path) "";
+        create_index html_prefix;
+        if length path > 1 then update_index parent_html_prefix name else ();
+        (case readme of NONE => () | SOME path => File.copy path html_prefix);
+        write_graph sorted_graph (Path.append html_prefix graph_path);
+        Isabelle_System.isabelle_tool "browser" "-b";
+        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
+        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
+          (HTML.applet_pages name (Url.File index_path, name));
+        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
+        List.app finish_html thys;
+        List.app (uncurry File.write) files;
+        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+        else ())
+      else ();
+
+    val _ =
+      (case dump_prefix of NONE => () | SOME (cp, path) =>
+       (prepare_sources cp path;
+        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
+        else ()));
+
+    val doc_paths =
+      documents |> Par_List.map (fn (name, tags) =>
+        let
+          val path = Path.append html_prefix (Path.basic name);
+          val _ = prepare_sources true path;
+        in isabelle_document true doc_format name tags path html_prefix end);
+    val _ =
+      if verbose then
+        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
+      else ();
   in
-    if info then
-     (Isabelle_System.mkdirs (Path.append html_prefix session_path);
-      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
-      File.write (Path.append html_prefix session_entries_path) "";
-      create_index html_prefix;
-      if length path > 1 then update_index parent_html_prefix name else ();
-      (case readme of NONE => () | SOME path => File.copy path html_prefix);
-      write_graph sorted_graph (Path.append html_prefix graph_path);
-      Isabelle_System.isabelle_tool "browser" "-b";
-      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
-      List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
-        (HTML.applet_pages name (Url.File index_path, name));
-      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
-      List.app finish_html thys;
-      List.app (uncurry File.write) files;
-      if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
-    else ();
-
-    (case doc_prefix2 of NONE => () | SOME (cp, path) =>
-     (prepare_sources cp path;
-      if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
-
-    (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
-      documents |> List.app (fn (name, tags) =>
-       let
-         val _ = prepare_sources true path;
-         val doc_path = isabelle_document true doc_format name tags path result_path;
-       in
-         if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
-       end));
-
     browser_info := empty_browser_info;
     session_info := NONE
-  end));
+  end);
 
 
 (* theory elements *)
@@ -462,7 +463,7 @@
 
     val files_html = files |> map (fn (raw_path, loadit) =>
       let
-        val path = #1 (Thy_Load.check_file dir raw_path);
+        val path = Thy_Load.check_file dir raw_path;
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,
--- a/src/Pure/Thy/term_style.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Thy/term_style.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -19,7 +19,7 @@
 fun err_dup_style name =
   error ("Duplicate declaration of antiquote style: " ^ quote name);
 
-structure StyleData = Theory_Data
+structure Styles = Theory_Data
 (
   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   val empty = Symtab.empty;
@@ -32,12 +32,12 @@
 (* accessors *)
 
 fun the_style thy name =
-  (case Symtab.lookup (StyleData.get thy) name of
+  (case Symtab.lookup (Styles.get thy) name of
     NONE => error ("Unknown antiquote style: " ^ quote name)
   | SOME (style, _) => style);
 
 fun setup name style thy =
-  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
+  Styles.map (Symtab.update_new (name, (style, stamp ()))) thy
     handle Symtab.DUP _ => err_dup_style name;
 
 
--- a/src/Pure/Thy/thy_header.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Thy/thy_header.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -7,7 +7,7 @@
 signature THY_HEADER =
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
-  val read: Position.T -> string -> string * string list * (string * bool) list
+  val read: Position.T -> string -> string * string list * (Path.T * bool) list
   val thy_path: string -> Path.T
   val split_thy_path: Path.T -> Path.T * string
   val consistent_name: string -> string -> unit
@@ -63,7 +63,8 @@
     |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
     |> Source.get_single;
   in
-    (case res of SOME (x, _) => x
+    (case res of
+      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
--- a/src/Pure/Thy/thy_info.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -232,7 +232,7 @@
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
-    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
+    val (_, _, uses) = Thy_Header.read pos text;
     fun init _ =
       Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
@@ -251,24 +251,20 @@
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_parents name, NONE)
+    SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
-      in (false, SOME (make_deps master imports), imports, SOME text) end
+      let val {master, text, imports, ...} = Thy_Load.check_thy dir name
+      in (false, SOME (make_deps master imports, text), imports) end
   | SOME (SOME {master, imports}) =>
-      let val master' = Thy_Load.check_thy dir name in
-        if #2 master <> #2 master' then
-          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
-          in (false, SOME (make_deps master' imports'), imports', SOME text') end
-        else
-          let
-            val current =
-              (case lookup_theory name of
-                NONE => false
-              | SOME theory => Thy_Load.all_current theory);
-            val deps' = SOME (make_deps master' imports);
-          in (current, deps', imports, NONE) end
-      end);
+      let
+        val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
+        val deps' = SOME (make_deps master' imports', text');
+        val current =
+          #2 master = #2 master' andalso
+            (case lookup_theory name of
+              NONE => false
+            | SOME theory => Thy_Load.all_current theory);
+      in (current, deps', imports') end);
 
 in
 
@@ -285,14 +281,15 @@
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
-          val (current, deps, imports, opt_text) = check_deps dir' name
+          val (current, deps, imports) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
 
           val parents = map base_name imports;
           val (parents_current, tasks') =
-            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
+            require_thys (name :: initiators)
+              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
@@ -300,10 +297,8 @@
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
-              | SOME (dep as {master = (thy_path, _), ...}) =>
-                  let
-                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
-                    val update_time = serial ();
+              | SOME (dep, text) =>
+                  let val update_time = serial ()
                   in Task (parents, load_thy initiators update_time dep text name) end);
         in (all_current, new_entry name parents task tasks') end)
   end;
@@ -336,7 +331,7 @@
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
     val imports = Thy_Load.imports_of theory;
     val deps = make_deps master imports;
--- a/src/Pure/Thy/thy_load.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -1,27 +1,25 @@
 (*  Title:      Pure/Thy/thy_load.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Loading files that contribute to a theory, including global load path
-management.
+Loading files that contribute to a theory.  Global master path.
 *)
 
 signature THY_LOAD =
 sig
-  val set_master_path: Path.T -> unit
-  val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
-  val check_thy: Path.T -> string -> Path.T * SHA1.digest
-  val deps_thy: Path.T -> string ->
-   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
+  val check_file: Path.T -> Path.T -> Path.T
+  val check_thy: Path.T -> string ->
+    {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
+  val set_master_path: Path.T -> unit
+  val get_master_path: unit -> Path.T
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -69,51 +67,25 @@
     else (master_dir, imports, required, (src_path, path_id) :: provided));
 
 
-(* stateful master path *)
-
-local
-  val master_path = Unsynchronized.ref Path.current;
-in
-
-fun set_master_path path = master_path := path;
-fun get_master_path () = ! master_path;
-
-end;
-
-
 (* check files *)
 
-fun get_file dir src_path =
+fun check_file dir file = File.check_file (File.full_path dir file);
+
+fun digest_file dir file =
   let
-    val path = Path.expand src_path;
-    val _ = Path.is_current path andalso error "Bad file specification";
-    val full_path = File.full_path (Path.append dir path);
-  in
-    if File.exists full_path
-    then SOME (full_path, SHA1.digest (File.read full_path))
-    else NONE
-  end;
-
-fun check_file dir file =
-  (case get_file dir file of
-    SOME path_id => path_id
-  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
+    val full_path = check_file dir file;
+    val id = SHA1.digest (File.read full_path);
+  in (full_path, id) end;
 
 fun check_thy dir name =
-  check_file dir (Thy_Header.thy_path name);
-
-
-(* theory deps *)
-
-fun deps_thy master_dir name =
   let
-    val master as (thy_path, _) = check_thy master_dir name;
-    val text = File.read thy_path;
-    val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
+    val master_file = check_file dir (Thy_Header.thy_path name);
+    val text = File.read master_file;
+    val (name', imports, uses) =
+      if name = Context.PureN then (Context.PureN, [], [])
+      else Thy_Header.read (Path.position master_file) text;
     val _ = Thy_Header.consistent_name name name';
-    val uses = map (Path.explode o #1) uses;
-  in {master = master, text = text, imports = imports, uses = uses} end;
-
+  in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 
 (* loaded files *)
@@ -138,7 +110,7 @@
   let
     val {master_dir, provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case get_file master_dir src_path of
+      (case try (digest_file master_dir) src_path of
         NONE => false
       | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
@@ -149,15 +121,15 @@
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, check_file (master_directory thy) src_path) thy;
+  provide (src_path, digest_file (master_directory thy) src_path) thy;
 
 fun use_ml src_path =
   if is_none (Context.thread_data ()) then
-    ML_Context.eval_file (#1 (check_file Path.current src_path))
+    ML_Context.eval_file (check_file Path.current src_path)
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, id) = check_file (master_directory thy) src_path;
+      val (path, id) = digest_file (master_directory thy) src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;
@@ -178,5 +150,16 @@
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
+
+(* global master path *)
+
+local
+  val master_path = Unsynchronized.ref Path.current;
+in
+
+fun set_master_path path = master_path := path;
+fun get_master_path () = ! master_path;
+
 end;
 
+end;
--- a/src/Pure/Tools/find_consts.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Tools/find_consts.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -69,7 +69,7 @@
 
 fun find_consts ctxt raw_criteria =
   let
-    val start = start_timing ();
+    val start = Timing.start ();
 
     val thy = ProofContext.theory_of ctxt;
     val low_ranking = 10000;
@@ -114,7 +114,7 @@
       |> sort (rev_order o int_ord o pairself snd)
       |> map (apsnd fst o fst);
 
-    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
     Pretty.str "" ::
--- a/src/Pure/Tools/find_theorems.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -464,7 +464,7 @@
 
 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
-    val start = start_timing ();
+    val start = Timing.start ();
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
@@ -480,7 +480,7 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
-    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     Pretty.str "" ::
--- a/src/Pure/theory.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Pure/theory.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -84,7 +84,7 @@
 
 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
-structure ThyData = Theory_Data_PP
+structure Thy = Theory_Data_PP
 (
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
@@ -104,9 +104,9 @@
     in make_thy (axioms', defs', (bgs', ens')) end;
 );
 
-fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
+fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
 
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
+fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
   make_thy (f (axioms, defs, wrappers)));
 
 
--- a/src/Tools/Code/code_haskell.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Tools/Code/code_haskell.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -350,7 +350,7 @@
     (*serialization*)
     fun write_module width (SOME destination) (module_name, content) =
           let
-            val _ = File.check destination;
+            val _ = File.check_dir destination;
             val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
               o separate "/" o Long_Name.explode) module_name;
             val _ = Isabelle_System.mkdirs (Path.dir filepath);
--- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Tools/quickcheck.ML	Mon Mar 21 08:29:16 2011 +0100
@@ -166,12 +166,9 @@
       error "Term to be tested contains schematic variables";
   in () end
 
-fun cpu_time description f =
-  let
-    val start = start_timing ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (end_timing start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 
 fun limit ctxt (limit_time, is_interactive) f exc () =
   if limit_time then