# HG changeset patch
# User wenzelm
# Date 1148674807 -7200
# Node ID 12f095315a4278d9415d296bb451373d280d57c8
# Parent  1c37d117a25d441e7a680abe3d6dd9787fef6893
removed unused extern_thm;

diff -r 1c37d117a25d -r 12f095315a42 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri May 26 22:20:06 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri May 26 22:20:07 2006 +0200
@@ -113,7 +113,6 @@
   val get_thms_closure: context -> thmref -> thm list
   val valid_thms: context -> string * thm list -> bool
   val lthms_containing: context -> FactIndex.spec -> (string * thm list) list
-  val extern_thm: context -> string -> xstring
   val no_base_names: context -> context
   val qualified_names: context -> context
   val sticky_prefix: string -> context -> context
@@ -1017,8 +1016,6 @@
 
 (* name space operations *)
 
-val extern_thm = NameSpace.extern o #1 o #1 o thms_of;
-
 val no_base_names   = map_naming NameSpace.no_base_names;
 val qualified_names = map_naming NameSpace.qualified_names;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;