Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sat, 04 Feb 2017 19:53:41 +0100
changeset 64984 2f72056cf78a
parent 64983 481b2855ee9a
child 64985 69592ac04836
tuned;
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions
src/Tools/solve_direct.ML file | annotate | diff | comparison | revisions 
--- 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) =
--- 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 =
isabelle