diff -r f8b933a62151 -r 3f8b24fcfbd6 src/Pure/Syntax/simple_syntax.ML --- a/src/Pure/Syntax/simple_syntax.ML Mon Jan 19 19:38:03 2009 +0100 +++ b/src/Pure/Syntax/simple_syntax.ML Mon Jan 19 20:05:41 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/Syntax/simple_syntax.ML - ID: $Id$ Author: Makarius Simple syntax for types and terms --- for bootstrapping Pure.