--- 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!?