diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/source.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Syntax/source.ML +(* Title: Pure/General/source.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen