# HG changeset patch
# User wenzelm
# Date 1486234421 -3600
# Node ID 2f72056cf78a648106fbfb82c8356aaf72fa9483
# Parent  481b2855ee9adc5488421520f73c8b6f77e851db
tuned;

diff -r 481b2855ee9a -r 2f72056cf78a src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Feb 04 19:48:43 2017 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 04 19:53:41 2017 +0100
@@ -475,7 +475,7 @@
 fun pretty_theorems state opt_limit rem_dups raw_criteria =
   let
     val ctxt = Proof.context_of state;
-    val opt_goal = try Proof.simple_goal state |> Option.map #goal;
+    val opt_goal = try (#goal o Proof.simple_goal) state;
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
 
     val (opt_found, theorems) =
diff -r 481b2855ee9a -r 2f72056cf78a src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Sat Feb 04 19:48:43 2017 +0100
+++ b/src/Tools/solve_direct.ML	Sat Feb 04 19:53:41 2017 +0100
@@ -61,9 +61,9 @@
       end;
 
     fun seek_against_goal () =
-      (case try Proof.simple_goal state of
+      (case try (#goal o Proof.simple_goal) state of
         NONE => NONE
-      | SOME {goal, ...} =>
+      | SOME goal =>
           let
             val subgoals = Drule.strip_imp_prems (Thm.cprop_of goal);
             val rs =