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 33095 bbd52d2f8696
parent 33039 5018f6a76b3f
child 33290 6dcb0a970783 
--- a/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -326,7 +326,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
+val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
 val qual_ord = int_ord o pairself (length o Long_Name.explode);
 val txt_ord = int_ord o pairself size;
 
@@ -355,7 +355,8 @@
     val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
 
     val shorten =
-      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
+      Name_Space.extern_flags
+        {long_names = false, short_names = false, unique_names = false} space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)
isabelle