--- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:37:04 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:50:29 2010 +0200
@@ -455,14 +455,6 @@
(** command syntax **)
-fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- let
- val proof_state = Toplevel.enter_proof_body state;
- val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
- in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
-
local
val criterion =
@@ -486,7 +478,13 @@
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
Keyword.diag
(options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
- >> (Toplevel.no_timing oo find_theorems_cmd));
+ >> (fn ((opt_lim, rem_dups), spec) =>
+ Toplevel.no_timing o
+ Toplevel.keep (fn state =>
+ let
+ val ctxt = Toplevel.context_of state;
+ val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+ in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
end;