# HG changeset patch
# User wenzelm
# Date 1395839734 -3600
# Node ID 9bc33476f6aca12f794a67eaa58b07dacd5b6da3
# Parent  1a91a0da65ab7d4c65e6ed374951e2de0afbbba3
unused;

diff -r 1a91a0da65ab -r 9bc33476f6ac src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Wed Mar 26 12:32:51 2014 +0100
+++ b/src/Pure/General/completion.ML	Wed Mar 26 14:15:34 2014 +0100
@@ -10,7 +10,6 @@
   val names: Position.T -> (string * (string * string)) list -> T
   val none: T
   val reported_text: T -> string
-  val report: T -> unit
   val suppress_abbrevs: string -> Markup.T list
 end;
 
@@ -46,8 +45,6 @@
     else ""
   end;
 
-val report = Output.report o reported_text;
-
 
 (* suppress short abbreviations *)