# HG changeset patch
# User wenzelm
# Date 1129751558 -7200
# Node ID 8e12d3a4b89035ab5ea4e330dd96aac774ec401b
# Parent  80a528111a82df183ea54f645f9241f77ba55e7e
removed obsolete old-style syntax;

diff -r 80a528111a82 -r 8e12d3a4b890 src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Wed Oct 19 21:52:37 2005 +0200
+++ b/src/HOLCF/cont_consts.ML	Wed Oct 19 21:52:38 2005 +0200
@@ -107,10 +107,4 @@
 
 end;
 
-
-(* old-style theory syntax *)
-
-val _ = ThySyn.add_syntax []
-  [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
-
 end;