merged
authorhaftmann
Thu, 18 Jun 2009 00:00:52 +0200
changeset 31699 b6710a3b4c49
parent 31695 36c5c15597f2 (diff)
parent 31698 9fc407df200c (current diff)
child 31700 b44912113c83
child 31707 678d294a563c
merged
--- a/Admin/isatest/settings/at-mac-poly-5.1-para	Wed Jun 17 17:42:46 2009 +0200
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para	Thu Jun 18 00:00:52 2009 +0200
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/polyml/polyml-svn"
-  ML_SYSTEM="polyml-experimental"
+  POLYML_HOME="/home/polyml/polyml-5.2.1"
+  ML_SYSTEM="polyml-5.2.1"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/doc-src/Classes/Thy/Classes.thy	Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Thu Jun 18 00:00:52 2009 +0200
@@ -5,8 +5,8 @@
 section {* Introduction *}
 
 text {*
-  Type classes were introduces by Wadler and Blott \cite{wadler89how}
-  into the Haskell language, to allow for a reasonable implementation
+  Type classes were introduced by Wadler and Blott \cite{wadler89how}
+  into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
   to classical Haskell 1.0 type classes, not considering
   later additions in expressiveness}.
@@ -43,9 +43,9 @@
 
   Indeed, type classes not only allow for simple overloading
   but form a generic calculus, an instance of order-sorted
-  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+  algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
 
-  From a software engeneering point of view, type classes
+  From a software engineering point of view, type classes
   roughly correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
@@ -65,7 +65,7 @@
 
   \end{quote}
 
-  \noindent From a theoretic point of view, type classes are lightweight
+  \noindent From a theoretical point of view, type classes are lightweight
   modules; Haskell type classes may be emulated by
   SML functors \cite{classes_modules}. 
   Isabelle/Isar offers a discipline of type classes which brings
@@ -77,22 +77,19 @@
     \item instantiating those abstract parameters by a particular
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
-    \item with a direct link to the Isabelle module system
-      (aka locales \cite{kammueller-locales}).
+    \item with a direct link to the Isabelle module system:
+      locales \cite{kammueller-locales}.
   \end{enumerate}
 
   \noindent Isar type classes also directly support code generation
-  in a Haskell like fashion.
+  in a Haskell like fashion. Internally, they are mapped to more primitive 
+  Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
 
   This tutorial demonstrates common elements of structured specifications
   and abstract reasoning with type classes by the algebraic hierarchy of
   semigroups, monoids and groups.  Our background theory is that of
   Isabelle/HOL \cite{isa-tutorial}, for which some
   familiarity is assumed.
-
-  Here we merely present the look-and-feel for end users.
-  Internally, those are mapped to more primitive Isabelle concepts.
-  See \cite{Haftmann-Wenzel:2006:classes} for more detail.
 *}
 
 section {* A simple algebra example \label{sec:example} *}
@@ -146,22 +143,22 @@
 end %quote
 
 text {*
-  \noindent @{command instantiation} allows to define class parameters
+  \noindent @{command instantiation} defines class parameters
   at a particular instance using common specification tools (here,
   @{command definition}).  The concluding @{command instance}
   opens a proof that the given parameters actually conform
   to the class specification.  Note that the first proof step
   is the @{method default} method,
   which for such instance proofs maps to the @{method intro_classes} method.
-  This boils down an instance judgement to the relevant primitive
-  proof goals and should conveniently always be the first method applied
+  This reduces an instance judgement to the relevant primitive
+  proof goals; typically it is the first method applied
   in an instantiation proof.
 
   From now on, the type-checker will consider @{typ int}
   as a @{class semigroup} automatically, i.e.\ any general results
   are immediately available on concrete instances.
 
-  \medskip Another instance of @{class semigroup} are the natural numbers:
+  \medskip Another instance of @{class semigroup} yields the natural numbers:
 *}
 
 instantiation %quote nat :: semigroup
@@ -191,7 +188,7 @@
 subsection {* Lifting and parametric types *}
 
 text {*
-  Overloaded definitions given on class instantiation
+  Overloaded definitions given at a class instantiation
   may include recursion over the syntactic structure of types.
   As a canonical example, we model product semigroups
   using our simple algebra:
@@ -201,11 +198,11 @@
 begin
 
 definition %quote
-  mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+  mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
 
 instance %quote proof
-  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
-  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+  fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+  show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
     unfolding mult_prod_def by (simp add: assoc)
 qed      
 
@@ -215,7 +212,7 @@
   \noindent Associativity of product semigroups is established using
   the definition of @{text "(\<otimes>)"} on products and the hypothetical
   associativity of the type components;  these hypotheses
-  are facts due to the @{class semigroup} constraints imposed
+  are legitimate due to the @{class semigroup} constraints imposed
   on the type components by the @{command instance} proposition.
   Indeed, this pattern often occurs with parametric types
   and type classes.
@@ -228,7 +225,7 @@
   We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
   by extending @{class semigroup}
   with one additional parameter @{text neutral} together
-  with its property:
+  with its characteristic property:
 *}
 
 class %quote monoidl = semigroup +
@@ -278,7 +275,7 @@
 end %quote
 
 text {*
-  \noindent Fully-fledged monoids are modelled by another subclass
+  \noindent Fully-fledged monoids are modelled by another subclass,
   which does not add new parameters but tightens the specification:
 *}
 
@@ -338,13 +335,13 @@
 
 section {* Type classes as locales *}
 
-subsection {* A look behind the scene *}
+subsection {* A look behind the scenes *}
 
 text {*
   The example above gives an impression how Isar type classes work
   in practice.  As stated in the introduction, classes also provide
   a link to Isar's locale system.  Indeed, the logical core of a class
-  is nothing else than a locale:
+  is nothing other than a locale:
 *}
 
 class %quote idem =
@@ -378,7 +375,7 @@
 proof qed (rule idem)
 
 text {*
-  \noindent This gives you at hand the full power of the Isabelle module system;
+  \noindent This gives you the full power of the Isabelle module system;
   conclusions in locale @{text idem} are implicitly propagated
   to class @{text idem}.
 *} (*<*)setup %invisible {* Sign.parent_path *}
@@ -435,25 +432,26 @@
 
   \noindent As you can see from this example, for local
   definitions you may use any specification tool
-  which works together with locales (e.g. \cite{krauss2006}).
+  which works together with locales, such as Krauss's recursive function package
+  \cite{krauss2006}.
 *}
 
 
 subsection {* A functor analogy *}
 
 text {*
-  We introduced Isar classes by analogy to type classes
+  We introduced Isar classes by analogy to type classes in
   functional programming;  if we reconsider this in the
   context of what has been said about type classes and locales,
   we can drive this analogy further by stating that type
-  classes essentially correspond to functors which have
+  classes essentially correspond to functors that have
   a canonical interpretation as type classes.
-  Anyway, there is also the possibility of other interpretations.
-  For example, also @{text list}s form a monoid with
+  There is also the possibility of other interpretations.
+  For example, @{text list}s also form a monoid with
   @{text append} and @{term "[]"} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinely algebraic types.
-  In such a case, we simply can do a particular interpretation
+  In such a case, we can simply make a particular interpretation
   of monoids for lists:
 *}
 
@@ -517,7 +515,7 @@
   to the type system, making @{text group} an instance of
   @{text monoid} by adding an additional edge
   to the graph of subclass relations
-  (cf.\ \figref{fig:subclass}).
+  (\figref{fig:subclass}).
 
   \begin{figure}[htbp]
    \begin{center}
@@ -550,7 +548,7 @@
   \end{figure}
 
   For illustration, a derived definition
-  in @{text group} which uses @{text pow_nat}:
+  in @{text group} using @{text pow_nat}
 *}
 
 definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -567,7 +565,7 @@
 subsection {* A note on syntax *}
 
 text {*
-  As a convenience, class context syntax allows to refer
+  As a convenience, class context syntax allows references
   to local class operations and their global counterparts
   uniformly;  type inference resolves ambiguities.  For example:
 *}
@@ -601,9 +599,9 @@
   @{command instantiation}
   targets naturally maps to Haskell type classes.
   The code generator framework \cite{isabelle-codegen} 
-  takes this into account.  Concerning target languages
-  lacking type classes (e.g.~SML), type classes
-  are implemented by explicit dictionary construction.
+  takes this into account.  If the target language (e.g.~SML)
+  lacks type classes, then they
+  are implemented by an explicit dictionary construction.
   As example, let's go back to the power function:
 *}
 
@@ -611,13 +609,13 @@
   "example = pow_int 10 (-2)"
 
 text {*
-  \noindent This maps to Haskell as:
+  \noindent This maps to Haskell as follows:
 *}
 
 text %quote {*@{code_stmts example (Haskell)}*}
 
 text {*
-  \noindent The whole code in SML with explicit dictionary passing:
+  \noindent The code in SML has explicit dictionary passing:
 *}
 
 text %quote {*@{code_stmts example (SML)}*}
--- a/doc-src/Classes/Thy/document/Classes.tex	Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Thu Jun 18 00:00:52 2009 +0200
@@ -23,8 +23,8 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Type classes were introduces by Wadler and Blott \cite{wadler89how}
-  into the Haskell language, to allow for a reasonable implementation
+Type classes were introduced by Wadler and Blott \cite{wadler89how}
+  into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
   to classical Haskell 1.0 type classes, not considering
   later additions in expressiveness}.
@@ -61,9 +61,9 @@
 
   Indeed, type classes not only allow for simple overloading
   but form a generic calculus, an instance of order-sorted
-  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+  algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
 
-  From a software engeneering point of view, type classes
+  From a software engineering point of view, type classes
   roughly correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
@@ -83,7 +83,7 @@
 
   \end{quote}
 
-  \noindent From a theoretic point of view, type classes are lightweight
+  \noindent From a theoretical point of view, type classes are lightweight
   modules; Haskell type classes may be emulated by
   SML functors \cite{classes_modules}. 
   Isabelle/Isar offers a discipline of type classes which brings
@@ -95,22 +95,19 @@
     \item instantiating those abstract parameters by a particular
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
-    \item with a direct link to the Isabelle module system
-      (aka locales \cite{kammueller-locales}).
+    \item with a direct link to the Isabelle module system:
+      locales \cite{kammueller-locales}.
   \end{enumerate}
 
   \noindent Isar type classes also directly support code generation
-  in a Haskell like fashion.
+  in a Haskell like fashion. Internally, they are mapped to more primitive 
+  Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
 
   This tutorial demonstrates common elements of structured specifications
   and abstract reasoning with type classes by the algebraic hierarchy of
   semigroups, monoids and groups.  Our background theory is that of
   Isabelle/HOL \cite{isa-tutorial}, for which some
-  familiarity is assumed.
-
-  Here we merely present the look-and-feel for end users.
-  Internally, those are mapped to more primitive Isabelle concepts.
-  See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
+  familiarity is assumed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -207,22 +204,22 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
   at a particular instance using common specification tools (here,
   \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   opens a proof that the given parameters actually conform
   to the class specification.  Note that the first proof step
   is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
   which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
-  This boils down an instance judgement to the relevant primitive
-  proof goals and should conveniently always be the first method applied
+  This reduces an instance judgement to the relevant primitive
+  proof goals; typically it is the first method applied
   in an instantiation proof.
 
   From now on, the type-checker will consider \isa{int}
   as a \isa{semigroup} automatically, i.e.\ any general results
   are immediately available on concrete instances.
 
-  \medskip Another instance of \isa{semigroup} are the natural numbers:%
+  \medskip Another instance of \isa{semigroup} yields the natural numbers:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -264,8 +261,8 @@
 \begin{isamarkuptext}%
 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
   in the primrec declaration;  by default, the local name of
-  a class operation \isa{f} to instantiate on type constructor
-  \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
+  a class operation \isa{f} to be instantiated on type constructor
+  \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
   these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
   or the corresponding ProofGeneral button.%
 \end{isamarkuptext}%
@@ -276,7 +273,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Overloaded definitions giving on class instantiation
+Overloaded definitions given at a class instantiation
   may include recursion over the syntactic structure of types.
   As a canonical example, we model product semigroups
   using our simple algebra:%
@@ -294,15 +291,15 @@
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
 \ \isacommand{proof}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
@@ -319,11 +316,10 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Associativity from product semigroups is
-  established using
+\noindent Associativity of product semigroups is established using
   the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
   associativity of the type components;  these hypotheses
-  are facts due to the \isa{semigroup} constraints imposed
+  are legitimate due to the \isa{semigroup} constraints imposed
   on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
   Indeed, this pattern often occurs with parametric types
   and type classes.%
@@ -338,7 +334,7 @@
 We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
   by extending \isa{semigroup}
   with one additional parameter \isa{neutral} together
-  with its property:%
+  with its characteristic property:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -439,7 +435,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Fully-fledged monoids are modelled by another subclass
+\noindent Fully-fledged monoids are modelled by another subclass,
   which does not add new parameters but tightens the specification:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -562,7 +558,7 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsubsection{A look behind the scene%
+\isamarkupsubsection{A look behind the scenes%
 }
 \isamarkuptrue%
 %
@@ -570,7 +566,7 @@
 The example above gives an impression how Isar type classes work
   in practice.  As stated in the introduction, classes also provide
   a link to Isar's locale system.  Indeed, the logical core of a class
-  is nothing else than a locale:%
+  is nothing other than a locale:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -714,7 +710,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent This gives you at hand the full power of the Isabelle module system;
+\noindent This gives you the full power of the Isabelle module system;
   conclusions in locale \isa{idem} are implicitly propagated
   to class \isa{idem}.%
 \end{isamarkuptext}%
@@ -832,7 +828,8 @@
 
   \noindent As you can see from this example, for local
   definitions you may use any specification tool
-  which works together with locales (e.g. \cite{krauss2006}).%
+  which works together with locales, such as Krauss's recursive function package
+  \cite{krauss2006}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -841,18 +838,18 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-We introduced Isar classes by analogy to type classes
+We introduced Isar classes by analogy to type classes in
   functional programming;  if we reconsider this in the
   context of what has been said about type classes and locales,
   we can drive this analogy further by stating that type
-  classes essentially correspond to functors which have
+  classes essentially correspond to functors that have
   a canonical interpretation as type classes.
-  Anyway, there is also the possibility of other interpretations.
-  For example, also \isa{list}s form a monoid with
+  There is also the possibility of other interpretations.
+  For example, \isa{list}s also form a monoid with
   \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinely algebraic types.
-  In such a case, we simply can do a particular interpretation
+  In such a case, we can simply make a particular interpretation
   of monoids for lists:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -982,7 +979,7 @@
   to the type system, making \isa{group} an instance of
   \isa{monoid} by adding an additional edge
   to the graph of subclass relations
-  (cf.\ \figref{fig:subclass}).
+  (\figref{fig:subclass}).
 
   \begin{figure}[htbp]
    \begin{center}
@@ -1015,7 +1012,7 @@
   \end{figure}
 
   For illustration, a derived definition
-  in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
+  in \isa{group} using \isa{pow{\isacharunderscore}nat}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1048,7 +1045,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-As a convenience, class context syntax allows to refer
+As a convenience, class context syntax allows references
   to local class operations and their global counterparts
   uniformly;  type inference resolves ambiguities.  For example:%
 \end{isamarkuptext}%
@@ -1113,9 +1110,9 @@
   \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
   targets naturally maps to Haskell type classes.
   The code generator framework \cite{isabelle-codegen} 
-  takes this into account.  Concerning target languages
-  lacking type classes (e.g.~SML), type classes
-  are implemented by explicit dictionary construction.
+  takes this into account.  If the target language (e.g.~SML)
+  lacks type classes, then they
+  are implemented by an explicit dictionary construction.
   As example, let's go back to the power function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -1136,7 +1133,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent This maps to Haskell as:%
+\noindent This maps to Haskell as follows:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1223,7 +1220,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent The whole code in SML with explicit dictionary passing:%
+\noindent The code in SML has explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1250,16 +1247,15 @@
 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a monoidl =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
+\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
+\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
+\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
+\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
@@ -1271,14 +1267,12 @@
 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
 \hspace*{0pt}\\
 \hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
 \hspace*{0pt} ~IntInf.int monoidl;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoid;\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
 \hspace*{0pt} ~IntInf.int group;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
--- a/doc-src/Classes/classes.tex	Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/classes.tex	Thu Jun 18 00:00:52 2009 +0200
@@ -21,8 +21,7 @@
 \maketitle
 
 \begin{abstract}
-  \noindent This tutorial introduces the look-and-feel of
-  Isar type classes to the end-user.  Isar type classes
+  \noindent This tutorial introduces Isar type classes, which 
   are a convenient mechanism for organizing specifications.
   Essentially, they combine an operational aspect (in the
   manner of Haskell) with a logical aspect, both managed uniformly.
--- a/doc-src/System/Thy/Presentation.thy	Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Thu Jun 18 00:00:52 2009 +0200
@@ -299,8 +299,8 @@
 
   \begin{center}\small
   \begin{tabular}{rcl}
-    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
-    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
+    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
   \end{tabular}
   \end{center}
 
@@ -454,6 +454,7 @@
     -p LEVEL     set level of detail for proof objects
     -r           reset session path
     -s NAME      override session NAME
+    -t BOOL      internal session timing (default false)
     -v BOOL      be verbose (default false)
 
   Build object-logic or run examples. Also creates browsing
@@ -563,6 +564,9 @@
   for internal proof objects, see also the \emph{Isabelle Reference
   Manual}~\cite{isabelle-ref}.
 
+  \medskip The @{verbatim "-t"} option produces a more detailed
+  internal timing report of the session.
+
   \medskip The @{verbatim "-v"} option causes additional information
   to be printed while running the session, notably the location of
   prepared documents.
--- a/doc-src/System/Thy/document/Presentation.tex	Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Thu Jun 18 00:00:52 2009 +0200
@@ -323,8 +323,8 @@
 
   \begin{center}\small
   \begin{tabular}{rcl}
-    \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
-    \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
+    \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
+    \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
   \end{tabular}
   \end{center}
 
@@ -480,6 +480,7 @@
     -p LEVEL     set level of detail for proof objects
     -r           reset session path
     -s NAME      override session NAME
+    -t BOOL      internal session timing (default false)
     -v BOOL      be verbose (default false)
 
   Build object-logic or run examples. Also creates browsing
@@ -580,6 +581,9 @@
   for internal proof objects, see also the \emph{Isabelle Reference
   Manual}~\cite{isabelle-ref}.
 
+  \medskip The \verb|-t| option produces a more detailed
+  internal timing report of the session.
+
   \medskip The \verb|-v| option causes additional information
   to be printed while running the session, notably the location of
   prepared documents.
--- a/lib/Tools/usedir	Wed Jun 17 17:42:46 2009 +0200
+++ b/lib/Tools/usedir	Thu Jun 18 00:00:52 2009 +0200
@@ -31,6 +31,7 @@
   echo "    -p LEVEL     set level of detail for proof objects"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
+  echo "    -t BOOL      internal session timing (default false)"
   echo "    -v BOOL      be verbose (default false)"
   echo
   echo "  Build object-logic or run examples. Also creates browsing"
@@ -84,12 +85,13 @@
 RESET=false
 SESSION=""
 PROOFS=0
+TIMING=false
 VERBOSE=false
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
+  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
   do
     case "$OPT" in
       C)
@@ -158,6 +160,10 @@
       s)
         SESSION="$OPTARG"
         ;;
+      t)
+        check_bool "$OPTARG"
+        TIMING="$OPTARG"
+        ;;
       v)
         check_bool "$OPTARG"
         VERBOSE="$OPTARG"
@@ -229,7 +235,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
+    -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;" \
     -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -238,7 +244,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
+    -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; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
--- a/lib/scripts/polyml-version	Wed Jun 17 17:42:46 2009 +0200
+++ b/lib/scripts/polyml-version	Thu Jun 18 00:00:52 2009 +0200
@@ -5,13 +5,8 @@
 echo -n polyml
 
 if [ -x "$ML_HOME/poly" ]; then
-  if [ -x "$ML_HOME/polyimport" ]; then
-    env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
-      DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
-      "$ML_HOME/poly" -v | \
-      sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
-  else
-    "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
-      sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
-  fi
+  env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
+    DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
+    "$ML_HOME/poly" -v -H 10 | \
+    sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
 fi
--- a/src/HOL/Tools/datatype_package/datatype_package.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -351,7 +351,7 @@
   simps : thm list}
 
 structure DatatypeInterpretation = InterpretationFun
-  (type T = datatype_config * string list val eq = eq_snd op =);
+  (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
 
 
--- a/src/Pure/General/output.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/General/output.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -18,7 +18,6 @@
   val timeap: ('a -> 'b) -> 'a -> 'b
   val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
   val timing: bool ref
-  val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
 end;
 
 signature OUTPUT =
@@ -47,7 +46,6 @@
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
-  val accumulated_time: unit -> unit
 end;
 
 structure Output: OUTPUT =
@@ -141,79 +139,9 @@
 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 = ref false;
 
-
-(* accumulated timing *)
-
-local
-
-datatype time_info = TI of
-  {name: string,
-   timer: Timer.cpu_timer,
-   sys: Time.time,
-   usr: Time.time,
-   gc: Time.time,
-   count: int};
-
-fun time_init name = ref (TI
- {name = name,
-  timer = Timer.startCPUTimer (),
-  sys = Time.zeroTime,
-  usr = Time.zeroTime,
-  gc = Time.zeroTime,
-  count = 0});
-
-fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
-
-fun time_check (ref (TI r)) = r;
-
-fun time_add ti f x =
-  let
-    fun add_diff time time1 time2 =
-      Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
-    val {name, timer, sys, usr, gc, count} = time_check ti;
-    val (sys1, usr1, gc1) = check_timer timer;
-    val result = Exn.capture f x;
-    val (sys2, usr2, gc2) = check_timer timer;
-  in
-    ti := TI
-     {name = name,
-      timer = timer,
-      sys = add_diff sys sys1 sys2,
-      usr = add_diff usr usr1 usr2,
-      gc = add_diff gc gc1 gc2,
-      count = count + 1};
-    Exn.release result
-  end;
-
-fun time_finish ti =
-  let
-    fun secs prfx time = prfx ^ Time.toString time;
-    val {name, timer, sys, usr, gc, count} = time_check ti;
-  in
-    warning ("Total of " ^ quote name ^ ": " ^
-      secs "User " usr ^ secs "  GC " gc ^ secs "  All " (Time.+ (sys, Time.+ (usr, gc))) ^
-      " secs in " ^ string_of_int count ^ " calls");
-    time_reset ti
-  end;
-
-val time_finish_hooks = ref ([]: (unit -> unit) list);
-
-in
-
-fun time_accumulator name =
-  let val ti = time_init name in
-    CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
-    time_add ti
-  end;
-
-fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
-
-end;
-
 end;
 
 structure BasicOutput: BASIC_OUTPUT = Output;
--- a/src/Pure/IsaMakefile	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Jun 18 00:00:52 2009 +0200
@@ -29,7 +29,8 @@
   ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
   ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
   ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
-  ML-Systems/time_limit.ML ML-Systems/universal.ML
+  ML-Systems/timing.ML ML-Systems/time_limit.ML				\
+  ML-Systems/universal.ML
 
 RAW: $(OUT)/RAW
 
--- a/src/Pure/ML-Systems/mosml.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -154,10 +154,6 @@
     val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
   in {message = message, user = user, all = all} end;
 
-fun check_timer timer =
-  let val {sys, usr, gc} = Timer.checkCPUTimer timer
-  in (sys, usr, gc) end;
-
 
 (* SML basis library fixes *)
 
--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -8,6 +8,7 @@
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
 val implode = SML90.implode;
 
 
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -12,6 +12,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
@@ -59,30 +60,6 @@
 end;
 
 
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
 (*prompts*)
 fun ml_prompts p1 p2 =
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/timing.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/ML-Systems/timing.ML
+    Author:     Makarius
+
+Compiler-independent timing functions.
+*)
+
+fun start_timing () =
+  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;
+
+fun end_timing (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;
+    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
+      Timer.checkCPUTimes cpu_timer;
+
+    open Time;
+    val elapsed = real_time2 - real_time;
+    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
+    val cpu = usr2 - usr + sys2 - sys + gc;
+    val gc_percent = Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * toReal gc / toReal cpu);
+    val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+    val message =
+      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
+        gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
+  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+
--- a/src/Pure/System/session.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/System/session.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -9,8 +9,9 @@
   val id: unit -> string list
   val name: unit -> string
   val welcome: unit -> string
-  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
-    string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
+  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+    string -> bool -> string list -> string -> string -> bool * string ->
+    string -> int -> bool -> bool -> int -> int -> bool -> unit
   val finish: unit -> unit
 end;
 
@@ -72,8 +73,7 @@
 (* finish *)
 
 fun finish () =
-  (Output.accumulated_time ();
-    ThyInfo.finish ();
+  (ThyInfo.finish ();
     Present.finish ();
     Future.shutdown ();
     session_finished := true);
@@ -92,13 +92,20 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
-fun use_dir root build modes reset info doc doc_graph doc_versions
-    parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
+fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+    name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
   ((fn () =>
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
-      use root;
+      if timing then
+        let
+          val start = start_timing ();
+          val _ = use root;
+          val stop = end_timing start;
+          val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+        in () end
+      else use root;
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
     |> setmp_noncritical print_mode (modes @ print_mode_value ())
--- a/src/Pure/Tools/find_consts.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -25,10 +25,9 @@
   | Loose of string
   | Name of string;
 
+
 (* matching types/consts *)
 
-fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
-
 fun matches_subtype thy typat =
   let
     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
@@ -51,7 +50,9 @@
 
 fun filter_const _ NONE = NONE
   | filter_const f (SOME (c, r)) =
-      Option.map (pair c o (curry Int.min r)) (f c);
+      (case f c of
+        NONE => NONE
+      | SOME i => SOME (c, Int.min (r, i)));
 
 
 (* pretty results *)
@@ -76,6 +77,7 @@
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;
 
+
 (* find_consts *)
 
 fun find_consts ctxt raw_criteria =
@@ -85,16 +87,17 @@
     val thy = ProofContext.theory_of ctxt;
     val low_ranking = 10000;
 
-    fun not_internal consts (nm, _) = 
+    fun not_internal consts (nm, _) =
       if member (op =) (Consts.the_tags consts nm) Markup.property_internal
       then NONE else SOME low_ranking;
 
     fun make_pattern crit =
       let
         val raw_T = Syntax.parse_typ ctxt crit;
-        val t = Syntax.check_term
-                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
-                  (Term.dummy_pattern raw_T);
+        val t =
+          Syntax.check_term
+            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+            (Term.dummy_pattern raw_T);
       in Term.type_of t end;
 
     fun make_match (Strict arg) =
@@ -102,34 +105,34 @@
             fn (_, (ty, _)) =>
               let
                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
-                val sub_size = Vartab.fold add_tye tye 0;
+                val sub_size =
+                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
               in SOME sub_size end handle MATCH => NONE
           end
-
       | make_match (Loose arg) =
           check_const (matches_subtype thy (make_pattern arg) o snd)
-      
       | make_match (Name arg) = check_const (match_string arg o fst);
 
     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
     val criteria = map make_criterion raw_criteria;
 
     val consts = Sign.consts_of thy;
-    val (_, consts_tab) = (#constants o Consts.dest) consts;
-    fun eval_entry c = fold filter_const (not_internal consts::criteria)
-                                         (SOME (c, low_ranking));
+    val (_, consts_tab) = #constants (Consts.dest consts);
+    fun eval_entry c =
+      fold filter_const (not_internal consts :: criteria)
+        (SOME (c, low_ranking));
 
     val matches =
       Symtab.fold (cons o eval_entry) consts_tab []
       |> map_filter I
       |> sort (rev_order o int_ord o pairself snd)
-      |> map ((apsnd fst) o fst);
+      |> map (apsnd fst o fst);
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
       :: Pretty.str ""
-      :: (Pretty.str o concat)
+      :: (Pretty.str o implode)
            (if null matches
             then ["nothing found", end_msg]
             else ["found ", (string_of_int o length) matches,
--- a/src/Pure/Tools/find_theorems.ML	Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -282,7 +282,7 @@
           in app (opt_add r r', consts', fs) end;
   in app end;
 
- 
+
 in
 
 fun filter_criterion ctxt opt_goal (b, c) =
@@ -417,7 +417,7 @@
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
     val returned = length thms;
-    
+
     val tally_msg =
       (case foundo of
         NONE => "displaying " ^ string_of_int returned ^ " theorems"
@@ -427,7 +427,7 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
         :: Pretty.str "" ::