author | kleing |
Sat, 10 Aug 2013 11:59:03 +0200 | |
changeset 52954 | b8b77a148ada |
parent 52953 | 2c927b7501c5 |
child 52955 | 797362ce0c14 |
--- 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