Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Tools/find_theorems.ML
changeset 52954 b8b77a148ada
parent 52943 14ddcc0ad7df
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
isabelle