eliminated obsolete heading category -- superseded by heading_level;
authorwenzelm
Wed, 10 Nov 2010 15:47:56 +0100
changeset 40459 913e545d9a9b
parent 40458 12c8c64203b3
child 40460 b6feba6c9fcc
eliminated obsolete heading category -- superseded by heading_level;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/keyword.scala	Wed Nov 10 15:43:06 2010 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Nov 10 15:47:56 2010 +0100
@@ -42,7 +42,6 @@
   val minor = Set(MINOR)
   val control = Set(CONTROL)
   val diag = Set(DIAG)
-  val heading = Set(THY_HEADING, PRF_HEADING)
   val theory =
     Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
       THY_GOAL, THY_SCHEMATIC_GOAL)
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:43:06 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:47:56 2010 +0100
@@ -38,12 +38,6 @@
       case None => false
     }
 
-  def is_heading(name: String): Boolean =
-    keyword_kind(name) match {
-      case Some(kind) => Keyword.heading(kind)
-      case None => false
-    }
-
   def heading_level(name: String): Option[Int] =
     name match {
       // FIXME avoid hard-wired info!?