proper headers;

--- a/src/Doc/Logics_ZF/If.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Doc/Logics_ZF/If.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Doc/ZF/If.thy
+(*  Title:      Doc/Logics_ZF/If.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 

--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_GHC.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on GHC

--- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_MLtonL.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_MLton.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on MLton

--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_OCaml.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on OCaml

--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_PolyML.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on PolyML

--- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_SMLNJ.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on SMLNJ

--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test_Scala.thy
+(*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test case for test_code on Scala

--- a/src/HOL/Inequalities.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Inequalities.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:     Inequalities
+(*  Title:     HOL/Inequalities.thy
     Author:    Tobias Nipkow
     Author:    Johannes Hölzl
 *)

--- a/src/HOL/Library/Code_Test.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Library/Code_Test.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test.thy
+(*  Title:      HOL/Library/Code_Test.thy
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test infrastructure for the code generator

--- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/ContNonDenum.thy
+(*  Title:      HOL/Library/ContNotDenum.thy
     Author:     Benjamin Porter, Monash University, NICTA, 2005
     Author:     Johannes Hölzl, TU München
 *)

--- a/src/HOL/Library/code_test.ML	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Library/code_test.ML	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Code_Test.ML
+(*  Title:      HOL/Library/code_test.ML
     Author:     Andreas Lochbihler, ETH Zurich
 
 Test infrastructure for the code generator

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
+(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Various tests for the proof reconstruction module.

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
+(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Unit tests for proof reconstruction module.

--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Transfer/transfer_bnf.ML
+(*  Title:      HOL/Tools/Lifting/lifting_bnf.ML
     Author:     Ondrej Kuncar, TU Muenchen
 
 Setup for Lifting for types that are BNF.

--- a/src/Pure/Concurrent/random.ML	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/Concurrent/random.ML	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Confurrent/random.ML
+(*  Title:      Pure/Concurrent/random.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Pseudo random numbers.

--- a/src/Pure/GUI/jfx_gui.scala	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/GUI/jfx_gui.scala	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/GUI/jfx_thread.scala
+/*  Title:      Pure/GUI/jfx_gui.scala
     Module:     PIDE-JFX
     Author:     Makarius
 

--- a/src/Pure/General/antiquote.scala	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/General/antiquote.scala	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/ML/antiquote.scala
+/*  Title:      Pure/General/antiquote.scala
     Author:     Makarius
 
 Antiquotations within plain text.

--- a/src/Pure/General/completion.ML	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/General/completion.ML	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Isar/completion.ML
+(*  Title:      Pure/General/completion.ML
     Author:     Makarius
 
 Semantic completion within the formal context.

--- a/src/Pure/PIDE/batch_session.scala	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/Tools/batch_session.scala
+/*  Title:      Pure/PIDE/batch_session.scala
     Author:     Makarius
 
 PIDE session in batch mode.

--- a/src/Pure/System/posix_interrupt.scala	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/System/posix_interrupt.scala	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/System/interrupt.scala
+/*  Title:      Pure/System/posix_interrupt.scala
     Author:     Makarius
 
 Support for POSIX interrupts (bypassed on Windows).

--- a/src/Pure/Tools/print_operation.scala	Mon Mar 16 16:26:33 2015 +0100
+++ b/src/Pure/Tools/print_operation.scala	Mon Mar 16 16:59:59 2015 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/System/print_operation.scala
+/*  Title:      Pure/Tools/print_operation.scala
     Author:     Makarius
 
 Print operations as asynchronous query.