diff r 3b549ee12623 r 6fce81e92e7c src/Pure/Tools/find_theorems.ML
 a/src/Pure/Tools/find_theorems.ML Fri Aug 09 15:00:29 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 09 15:14:59 2013 +0200
@@ 164,7 +164,7 @@
is_nontrivial thy pat andalso
Pattern.matches thy (if po then (pat, obj) else (obj, pat));
 fun substsize pat =
+ fun subst_size pat =
let val (_, subst) =
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
@@ 174,7 +174,7 @@
val match_thm = matches o refine_term;
in
 map (substsize o refine_term) (filter match_thm (extract_terms term_src))
+ map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
> bestmatch
end;
@@ 275,16 +275,13 @@
fun get_names t = Term.add_const_names t (Term.add_free_names t []);
(*Including all constants and frees is only sound because
 matching uses higherorder patterns. If full matching
 were used, then constants that may be subject to
 betareduction after substitution of frees should
 not be included for LHS set because they could be
 thrown away by the substituted function.
 e.g. for (?F 1 2) do not include 1 or 2, if it were
 possible for ?F to be (% x y. 3)
 The largest possible set should always be included on
 the RHS.*)
+(*Including all constants and frees is only sound because matching
+ uses higherorder patterns. If full matching were used, then
+ constants that may be subject to betareduction after substitution
+ of frees should not be included for LHS set because they could be
+ thrown away by the substituted function. E.g. for (?F 1 2) do not
+ include 1 or 2, if it were possible for ?F to be (%x y. 3). The
+ largest possible set should always be included on the RHS.*)
fun filter_pattern ctxt pat =
let
@@ 305,16 +302,14 @@
fun err_no_goal c =
error ("Current goal required for " ^ c ^ " search criterion");
val fix_goal = Thm.prop_of;

fun filter_crit _ _ (Name name) = apfst (filter_name name)
 filter_crit _ NONE Intro = err_no_goal "intro"
 filter_crit _ NONE Elim = err_no_goal "elim"
 filter_crit _ NONE Dest = err_no_goal "dest"
 filter_crit _ NONE Solves = err_no_goal "solves"
  filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
  filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
  filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
+  filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
+  filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
+  filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
 filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
@@ 365,7 +360,7 @@
end;
(* removing duplicates, preferring nicer names, roughly n log n *)
+(* removing duplicates, preferring nicer names, roughly O(n log n) *)
local
@@ 412,7 +407,7 @@
in nicer end;
fun rem_thm_dups nicer xs =
 xs ~~ (1 upto length xs)
+ (xs ~~ (1 upto length xs))
> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
> rem_cdups nicer
> sort (int_ord o pairself #2)
@@ 500,13 +495,13 @@
fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
 val (foundo, theorems) =
+ val (opt_found, theorems) =
filter_theorems ctxt (map Internal (all_facts_of ctxt))
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;
val tally_msg =
 (case foundo of
+ (case opt_found of
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
 SOME found =>
"found " ^ string_of_int found ^ " theorem(s)" ^