# HG changeset patch
# User wenzelm
# Date 1127217821 -7200
# Node ID 854d061f6c1077f2a403aa713e7d3aaed846741d
# Parent  51314f4bd01daacd20322c2675c48feb0a584901
removed obsolete thms_containing;

diff -r 51314f4bd01d -r 854d061f6c10 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 20 14:03:40 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 20 14:03:41 2005 +0200
@@ -689,13 +689,6 @@
      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
 
-val thms_containingP =   (* FIXME legacy *)
-  OuterSyntax.improper_command "thms_containing"
-    "print theorems meeting specified criteria" K.diag
-    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
-     Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-      >> (Toplevel.no_timing oo IsarCmd.find_theorems));
-
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -868,7 +861,6 @@
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,
   print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
-  thms_containingP,  (* FIXME legacy *)
   print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP,
   print_full_prfsP, print_propP, print_termP, print_typeP,
   (*system commands*)