1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 20 14:03:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 20 14:03:41 2005 +0200
     1.3 @@ -689,13 +689,6 @@
     1.4       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
     1.5        >> (Toplevel.no_timing oo IsarCmd.find_theorems));
     1.6  
     1.7 -val thms_containingP =   (* FIXME legacy *)
     1.8 -  OuterSyntax.improper_command "thms_containing"
     1.9 -    "print theorems meeting specified criteria" K.diag
    1.10 -    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
    1.11 -     Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.12 -      >> (Toplevel.no_timing oo IsarCmd.find_theorems));
    1.13 -
    1.14  val print_bindsP =
    1.15    OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
    1.16      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
    1.17 @@ -868,7 +861,6 @@
    1.18    print_registrationsP, print_attributesP, print_simpsetP,
    1.19    print_rulesP, print_induct_rulesP, print_trans_rulesP,
    1.20    print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
    1.21 -  thms_containingP,  (* FIXME legacy *)
    1.22    print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP,
    1.23    print_full_prfsP, print_propP, print_termP, print_typeP,
    1.24    (*system commands*)