# HG changeset patch
# User kleing
# Date 1376128743 -7200
# Node ID b8b77a148ada0c95f80120aa697bf6d7da54a544
# Parent  2c927b7501c58ec445d26c856a485b0713c95c7f
use local context for name space

diff -r 2c927b7501c5 -r b8b77a148ada src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Aug 10 10:59:56 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Aug 10 11:59:03 2013 +0200
@@ -376,8 +376,7 @@
 
 fun nicer_shortest ctxt =
   let
-    (* FIXME Why global name space!?? *)
-    val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
+    val space = Facts.space_of (Proof_Context.facts_of ctxt);
 
     val shorten =
       Name_Space.extern