src/Pure/pure_syn.ML
changeset 62453 b93cc7d73431
parent 61464 d35ff80f27fb
child 62876 507c90523113
--- a/src/Pure/pure_syn.ML	Sun Feb 28 15:57:03 2016 +0100
+++ b/src/Pure/pure_syn.ML	Sun Feb 28 17:37:20 2016 +0100
@@ -14,10 +14,6 @@
 struct
 
 val _ =
-  Outer_Syntax.command ("header", @{here}) "theory header"
-    (Parse.document_source >> Thy_Output.old_header_command);
-
-val _ =
   Outer_Syntax.command ("chapter", @{here}) "chapter heading"
     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});