# HG changeset patch
# User wenzelm
# Date 1436130170 -7200
# Node ID 65911ba3da23d4a418877eb0abcba72ce584f16d
# Parent  1049f3724ac0664cd998c6c54da7efc518234acb
obsolete;

diff -r 1049f3724ac0 -r 65911ba3da23 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Jul 05 23:01:33 2015 +0200
+++ b/src/Pure/display.ML	Sun Jul 05 23:02:50 2015 +0200
@@ -21,10 +21,8 @@
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thm_item: Proof.context -> thm -> Pretty.T
   val pretty_thm_global: theory -> thm -> Pretty.T
-  val pretty_thm_without_context: thm -> Pretty.T
   val string_of_thm: Proof.context -> thm -> string
   val string_of_thm_global: theory -> thm -> string
-  val string_of_thm_without_context: thm -> string
   val pretty_full_theory: bool -> theory -> Pretty.T list
 end;
 
@@ -82,11 +80,8 @@
 fun pretty_thm_global thy =
   pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
 
-fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
-
 val string_of_thm = Pretty.string_of oo pretty_thm;
 val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
-val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;