# HG changeset patch
# User blanchet
# Date 1406902053 -7200
# Node ID a30a3d5aaec209cd0f3578c9bc0bc56e16dfcac0
# Parent  92fe49c7ab3bcf7f1cef52dd832674abcd5659ae
tuning

diff -r 92fe49c7ab3b -r a30a3d5aaec2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 16:07:33 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 16:07:33 2014 +0200
@@ -974,8 +974,8 @@
   thms_in_proof max_dependencies (SOME name_tabs) th
   |> Option.map (fn deps =>
     if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
-       exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
-       is_size_def deps th then
+        exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
+        is_size_def deps th then
       []
     else
       deps)
@@ -1378,7 +1378,7 @@
             let
               val name = nickname_of_thm th
               val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
-              val deps = deps_of status th |> these
+              val deps = these (deps_of status th)
               val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
               val learns = (name, parents, feats, deps) :: learns
               val (learns, next_commit) =