# HG changeset patch
# User wenzelm
# Date 1289400476 -3600
# Node ID 913e545d9a9b060d534983892114c308d8694947
# Parent  12c8c64203b3760d16834bfdd866bab668235a99
eliminated obsolete heading category -- superseded by heading_level;

diff -r 12c8c64203b3 -r 913e545d9a9b src/Pure/Isar/keyword.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)
diff -r 12c8c64203b3 -r 913e545d9a9b src/Pure/Isar/outer_syntax.scala
--- 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!?