--- a/src/Pure/Tools/find_consts.ML Wed Aug 11 17:37:04 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 17:50:29 2010 +0200
@@ -144,19 +144,22 @@
(* command syntax *)
-fun find_consts_cmd spec =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
+local
val criterion =
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
Parse.xname >> Loose;
+in
+
val _ =
Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
(Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
- >> (Toplevel.no_timing oo find_consts_cmd));
+ >> (fn spec => Toplevel.no_timing o
+ Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
end;
+end;
+
--- 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;