Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Tools/find_theorems.ML
changeset 64984 2f72056cf78a
parent 64983 481b2855ee9a
child 67147 dea94b1aabc3 
--- 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) =
isabelle