# HG changeset patch
# User wenzelm
# Date 1281541829 -7200
# Node ID c677c2c1d333addf6d76a394ca5bed304eb78bd9
# Parent  3f4fadad94973451cd74bf5e2a3035d82d7b5335
simplified/unified command setup;

diff -r 3f4fadad9497 -r c677c2c1d333 src/Pure/Tools/find_consts.ML
--- 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;
+
diff -r 3f4fadad9497 -r c677c2c1d333 src/Pure/Tools/find_theorems.ML
--- 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;