# HG changeset patch
# User haftmann
# Date 1278598764 -7200
# Node ID 3daaf23b9ab4ec43ad79a99559ee3efbdbb9d103
# Parent  0a3fa8fbcdc5dcd9e8f3b1e1a83257bfb375d85f
tuned titles

diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/FOLP/classical.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/classical
+(*  Title:      FOLP/classical.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/FOLP/hypsubst.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/hypsubst
+(*  Title:      FOLP/hypsubst.ML
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Amine Chaieb
+(*  Title:      HOL/Decision_Procs/commutative_ring_tac.ML
+    Author:     Amine Chaieb
 
 Tactic for solving equalities over commutative rings.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
+(* Title:      HOL/Decision_Procs/ferrante_rackoff.ML
    Author:     Amine Chaieb, TU Muenchen
 
 Ferrante and Rackoff's algorithm for quantifier elimination in dense
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Decision_Procs/ferrante_rackoff_data.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
+(* Title:      HOL/Decision_Procs/ferrante_rackoff_data.ML
    Author:     Amine Chaieb, TU Muenchen
 
 Context data for Ferrante and Rackoff's algorithm for quantifier
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Qelim/langford.ML
+(*  Title:      HOL/Decision_Procs/langford.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title:      positivstellensatz_tools.ML
+(* Title:      HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
    Author:     Philipp Meyer, TU Muenchen
 
 Functions for generating a certificate from a positivstellensatz and vice versa
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Library/reify_data.ML
--- a/src/HOL/Library/reify_data.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Library/reify_data.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/reflection_data.ML
+(*  Title:      HOL/Library/reify_data.ML
     Author:     Amine Chaieb, TU Muenchen
 
 Data for the reification and reflection methods.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Library/normarith.ML
+(*  Title:      HOL/Multivariate_Analysis/normarith.ML
     Author:     Amine Chaieb, University of Cambridge
 
 Simple decision procedure for linear problems in Euclidean space.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,5 +1,4 @@
-(*
-    Title:      HOL/Mutabelle/mutabelle.ML
+(*  Title:      HOL/Mutabelle/mutabelle.ML
     Author:     Veronika Ortner, TU Muenchen
 
     Mutation of theorems
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,5 +1,4 @@
-(*
-    Title:      HOL/Mutabelle/mutabelle_extra.ML
+(*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
 
     Invokation of Counterexample generators
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/NSA/transfer.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,5 @@
-(*  Title       : HOL/Hyperreal/transfer.ML
-    ID          : $Id$
-    Author      : Brian Huffman
+(*  Title:      HOL/NSA/transfer.ML
+    Author:     Brian Huffman
 
 Transfer principle tactic for nonstandard analysis.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Function/fundef.ML
+(*  Title:      HOL/Tools/Function/function.ML
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Function/fundef_lib.ML
+(*  Title:      HOL/Tools/Function/function_lib.ML
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Function/fundef_datatype.ML
+(*  Title:      HOL/Tools/Function/pat_completeness.ML
     Author:     Alexander Krauss, TU Muenchen
 
 Method "pat_completeness" to prove completeness of datatype patterns.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Quotient/quotient_def.thy
+(*  Title:      HOL/Tools/Quotient/quotient_def.ML
     Author:     Cezary Kaliszyk and Christian Urban
 
 Definitions for constants on quotient types.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Quotient/quotient_info.thy
+(*  Title:      HOL/Tools/Quotient/quotient_info.ML
     Author:     Cezary Kaliszyk and Christian Urban
 
 Data slots for the quotient package.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
+(*  Title:      HOL/Tools/Quotient/quotient_tacs.ML
     Author:     Cezary Kaliszyk and Christian Urban
 
 Tactics for solving goal arising from lifting theorems to quotient
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Quotient/quotient_term.thy
+(*  Title:      HOL/Tools/Quotient/quotient_term.ML
     Author:     Cezary Kaliszyk and Christian Urban
 
 Constructs terms corresponding to goals from lifting theorems to
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
+(*  Title:      HOL/Tools/Quotient/quotient_typ.ML
     Author:     Cezary Kaliszyk and Christian Urban
 
 Definition of a quotient type.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/float_syntax.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Tobias Nipkow, TU Muenchen
+(*  Title:      HOL/Tools/float_syntax.ML
+    Author:     Tobias Nipkow, TU Muenchen
 
 Concrete syntax for floats.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
+(*  Title:      HOL/Tools/groebner.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/hologic.ML
+(*  Title:      HOL/Tools/hologic.ML
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Abstract syntax operations for HOL.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(*  Title:  HOL/Tools/list_code.ML
+    Author: Florian Haftmann, TU Muenchen
 
 Code generation for list literals.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(*  Title:      HOL/Tools/quickcheck_generators.ML
+    Author:     Florian Haftmann, TU Muenchen
 
 Quickcheck generators for various types.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
+(*  Title:      HOL/Tools/semiring_normalizer.ML
     Author:     Amine Chaieb, TU Muenchen
 
 Normalization of expressions in semirings.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/simpdata.ML
+(*  Title:      HOL/Tools/simpdata.ML
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/string_code.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(*  Title:      HOL/Tools/string_code.ML
+    Author:     Florian Haftmann, TU Muenchen
 
 Code generation for character and string literals.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/transfer.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,7 @@
-(*  Author:   Amine Chaieb, University of Cambridge, 2009
-              Jeremy Avigad, Carnegie Mellon University
-              Florian Haftmann, TU Muenchen
+(*  Title:      HOL/Tools/transfer.ML
+    Author:     Amine Chaieb, University of Cambridge, 2009
+                Jeremy Avigad, Carnegie Mellon University
+                Florian Haftmann, TU Muenchen
 
 Simple transfer principle on theorems.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/domain/domain_constructors.ML
+(*  Title:      HOLCF/Tools/Domain/domain_constructors.ML
     Author:     Brian Huffman
 
 Defines constructor functions for a given domain isomorphism
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/domain/domain_isomorphism.ML
+(*  Title:      HOLCF/Tools/Domain/domain_isomorphism.ML
     Author:     Brian Huffman
 
 Defines new types satisfying the given domain equations.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
+(*  Title:      HOLCF/Tools/Domain/domain_take_proofs.ML
     Author:     Brian Huffman
 
 Defines take functions for the given domain equation
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Provers/order.ML
--- a/src/Provers/order.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/order.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Oliver Kutter, TU Muenchen
+(*  Title:      Provers/order.ML
+    Author:     Oliver Kutter, TU Muenchen
 
 Transitivity reasoner for partial and linear orders.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/quasi.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Oliver Kutter, TU Muenchen
+(*  Title:      Provers/quasi.ML
+    Author:     Oliver Kutter, TU Muenchen
 
 Reasoner for simple transitivity and quasi orders.
 *)
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/trancl.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,7 @@
-(*
-    Title:      Transitivity reasoner for transitive closures of relations
+(*  Title:      Provers/trancl.ML
     Author:     Oliver Kutter, TU Muenchen
+
+Transitivity reasoner for transitive closures of relations
 *)
 
 (*
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_eval.ML
+(*  Title:      Tools/Code/code_eval.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Runtime services building on code generation into implementation language SML.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_preproc.ML
+(*  Title:      Tools/Code/code_preproc.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Preprocessing code equations into a well-sorted system
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_printer.ML
+(*  Title:      Tools/Code/code_printer.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Generic operations for pretty printing of target language code.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_simp.ML
+(*  Title:      Tools/Code/code_simp.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Connecting the simplifier and the code generator.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_thingol.ML
+(*  Title:      Tools/Code/code_thingol.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Intermediate language ("Thin-gol") representing executable code.
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/WWW_Find/html_unicode.ML
--- a/src/Tools/WWW_Find/html_unicode.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      html_unicode.ML
+(*  Title:      Tools/WWW_Find/html_unicode.ML
     Author:     Timothy Bourke, NICTA
                 Based on Pure/Thy/html.ML
                 by Markus Wenzel and Stefan Berghofer, TU Muenchen
diff -r 0a3fa8fbcdc5 -r 3daaf23b9ab4 src/Tools/value.ML
--- a/src/Tools/value.ML	Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/value.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/value.ML
+(*  Title:      Tools/value.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Generic value command for arbitrary evaluators.