--- a/src/HOL/thy_syntax.ML Sun Nov 04 21:00:28 2001 +0100
+++ b/src/HOL/thy_syntax.ML Sun Nov 04 21:12:03 2001 +0100
@@ -2,7 +2,7 @@
ID: $Id$
Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
-Additional theory file sections for HOL.
+Additional sections for *old-style* theory files in HOL.
*)
local
--- a/src/ZF/thy_syntax.ML Sun Nov 04 21:00:28 2001 +0100
+++ b/src/ZF/thy_syntax.ML Sun Nov 04 21:12:03 2001 +0100
@@ -3,13 +3,11 @@
Author: Lawrence C Paulson
Copyright 1994 University of Cambridge
-Additional theory file sections for ZF.
+Additional sections for *old-style* theory files in ZF.
*)
-
local
-
open ThyParse;
(*ML identifiers for introduction rules.*)