# HG changeset patch
# User wenzelm
# Date 1376054099 -7200
# Node ID 6fce81e92e7caa9ca732da128b5e20eb84361971
# Parent  3b549ee126231f09231b1310adde45521bcf2692
tuned;

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 higher-order patterns. If full matching
-  were used, then constants that may be subject to
-  beta-reduction 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 higher-order patterns. If full matching were used, then
+  constants that may be subject to beta-reduction 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)" ^