removed obsolete old-style syntax;
authorwenzelm
Wed, 19 Oct 2005 21:52:38 +0200
changeset 17926 8e12d3a4b890
parent 17925 80a528111a82
child 17927 4b42562ec171
removed obsolete old-style syntax;
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;