# HG changeset patch # User wenzelm # Date 1428078979 -7200 # Node ID f673ce6b1e2b71cce98b155620c650d48b74bfd1 # Parent 7d5b2f4c621c6f2ce4d22fb2589753e6187c3334 tuned; diff -r 7d5b2f4c621c -r f673ce6b1e2b src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Apr 02 20:46:44 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Apr 03 18:36:19 2015 +0200 @@ -476,7 +476,7 @@ fun add_facts global foldx facts = foldx (fn (name0, ths) => fn accum => if name0 <> "" andalso - (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse + (Long_Name.is_hidden (Facts.intern facts name0) orelse ((Facts.is_concealed facts name0 orelse (not generous andalso is_blacklisted_or_something name0)) andalso forall (not o member Thm.eq_thm_prop add_ths) ths)) then diff -r 7d5b2f4c621c -r f673ce6b1e2b src/Pure/General/long_name.ML --- a/src/Pure/General/long_name.ML Thu Apr 02 20:46:44 2015 +0200 +++ b/src/Pure/General/long_name.ML Fri Apr 03 18:36:19 2015 +0200 @@ -9,6 +9,7 @@ val separator: string val is_qualified: string -> bool val hidden: string -> string + val is_hidden: string -> bool val dest_hidden: string -> string option val localN: string val dest_local: string -> string option @@ -29,8 +30,10 @@ val is_qualified = exists_string (fn s => s = separator); -val hidden = prefix "??."; -val dest_hidden = try (unprefix "??."); +val hidden_prefix = "??." +val hidden = prefix hidden_prefix; +val is_hidden = String.isPrefix hidden_prefix; +val dest_hidden = try (unprefix hidden_prefix); val localN = "local"; val dest_local = try (unprefix "local."); diff -r 7d5b2f4c621c -r f673ce6b1e2b src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Apr 02 20:46:44 2015 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Apr 03 18:36:19 2015 +0200 @@ -328,7 +328,7 @@ local val index_ord = option_ord (K EQUAL); -val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden); +val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; val qual_ord = int_ord o apply2 Long_Name.qualification; val txt_ord = int_ord o apply2 size;