# HG changeset patch
# User wenzelm
# Date 1565944405 -7200
# Node ID b93ba98e627a8fef49421c6d2f1be34f78eb6fc5
# Parent  16e98f89a29c6ef01e24245754bdd8e7a966fbe3
tuned signature;

diff -r 16e98f89a29c -r b93ba98e627a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 16 10:20:41 2019 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 10:33:25 2019 +0200
@@ -282,7 +282,7 @@
         val atts = map (attribute_generic context) srcs;
         val (ths', context') =
           fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
-      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
+      in (context', pick (name, Facts.ref_pos thmref) ths') end)
   end);
 
 in
diff -r 16e98f89a29c -r b93ba98e627a src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 16 10:20:41 2019 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 16 10:33:25 2019 +0200
@@ -125,7 +125,7 @@
 (* filter_name *)
 
 fun filter_name str_pat (thmref, _) =
-  if match_string str_pat (Facts.name_of_ref thmref)
+  if match_string str_pat (Facts.ref_name thmref)
   then SOME (0, 0, 0) else NONE;
 
 
diff -r 16e98f89a29c -r b93ba98e627a src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri Aug 16 10:20:41 2019 +0200
+++ b/src/Pure/facts.ML	Fri Aug 16 10:33:25 2019 +0200
@@ -12,11 +12,11 @@
     Named of (string * Position.T) * interval list option |
     Fact of string
   val named: string -> ref
+  val ref_name: ref -> string
+  val ref_pos: ref -> Position.T
+  val map_ref_name: (string -> string) -> ref -> ref
   val string_of_selection: interval list option -> string
   val string_of_ref: ref -> string
-  val name_of_ref: ref -> string
-  val pos_of_ref: ref -> Position.T
-  val map_name_of_ref: (string -> string) -> ref -> ref
   val select: ref -> thm list -> thm list
   val selections: string * thm list -> (ref * thm) list
   type T
@@ -85,14 +85,14 @@
 
 fun named name = Named ((name, Position.none), NONE);
 
-fun name_of_ref (Named ((name, _), _)) = name
-  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
+fun ref_name (Named ((name, _), _)) = name
+  | ref_name (Fact _) = raise Fail "Illegal literal fact";
 
-fun pos_of_ref (Named ((_, pos), _)) = pos
-  | pos_of_ref (Fact _) = Position.none;
+fun ref_pos (Named ((_, pos), _)) = pos
+  | ref_pos (Fact _) = Position.none;
 
-fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
-  | map_name_of_ref _ r = r;
+fun map_ref_name f (Named ((name, pos), is)) = Named ((f name, pos), is)
+  | map_ref_name _ r = r;
 
 fun string_of_selection NONE = ""
   | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));