use local context for name space
authorkleing
Sat Aug 10 11:59:03 2013 +0200 (2013-08-10)
changeset 52954b8b77a148ada
parent 52953 2c927b7501c5
child 52955 797362ce0c14
use local context for name space
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Aug 10 10:59:56 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Aug 10 11:59:03 2013 +0200
     1.3 @@ -376,8 +376,7 @@
     1.4  
     1.5  fun nicer_shortest ctxt =
     1.6    let
     1.7 -    (* FIXME Why global name space!?? *)
     1.8 -    val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
     1.9 +    val space = Facts.space_of (Proof_Context.facts_of ctxt);
    1.10  
    1.11      val shorten =
    1.12        Name_Space.extern