src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 27 12:28:28 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 27 15:46:22 2009 +0100
@@ -37,6 +37,7 @@
     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
 
 
+
 (** markup commands **)
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
@@ -79,7 +80,7 @@
 
 
 
-(** theory sections **)
+(** theory commands **)
 
 (* classes and sorts *)
 
@@ -853,47 +854,6 @@
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
 
-local
-
-val criterion =
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
-  P.reserved "intro" >> K FindTheorems.Intro ||
-  P.reserved "elim" >> K FindTheorems.Elim ||
-  P.reserved "dest" >> K FindTheorems.Dest ||
-  P.reserved "solves" >> K FindTheorems.Solves ||
-  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
-  P.term >> FindTheorems.Pattern;
-
-val options =
-  Scan.optional
-    (P.$$$ "(" |--
-      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
-        --| P.$$$ ")")) (NONE, true);
-in
-
-val _ =
-  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
-    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-      >> (Toplevel.no_timing oo IsarCmd.find_theorems));
-
-end;
-
-local
-
-val criterion =
-  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict ||
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name ||
-  P.xname >> FindConsts.Loose;
-
-in
-
-val _ =
-  OuterSyntax.improper_command "find_consts" "search constants by type pattern"
-    K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-            >> (Toplevel.no_timing oo IsarCmd.find_consts));
-
-end;
-
 val _ =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -948,6 +908,7 @@
          (Toplevel.no_timing oo IsarCmd.unused_thms));
 
 
+
 (** system commands (for interactive mode only) **)
 
 val _ =