--- 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*)