# HG changeset patch
# User wenzelm
# Date 1394031971 -3600
# Node ID 41e06ec17604b8f52fd7bdd8b0fd6f180e5ae00c
# Parent  5438ed05e1c9ae71de93b10be7666fcd365a2480
unused;

diff -r 5438ed05e1c9 -r 41e06ec17604 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Mar 05 15:25:52 2014 +0100
+++ b/src/Pure/General/pretty.ML	Wed Mar 05 16:06:11 2014 +0100
@@ -42,7 +42,6 @@
   val text_fold: T list -> T
   val keyword1: string -> T
   val keyword2: string -> T
-  val keyword3: string -> T
   val text: string -> T list
   val paragraph: T list -> T
   val para: string -> T
@@ -166,7 +165,6 @@
 
 fun keyword1 name = mark_str (Markup.keyword1, name);
 fun keyword2 name = mark_str (Markup.keyword2, name);
-fun keyword3 name = mark_str (Markup.keyword3, name);
 
 val text = breaks o map str o Symbol.explode_words;
 val paragraph = markup Markup.paragraph;