--- a/src/Pure/Isar/isar_syn.ML Tue Jul 02 17:00:05 2002 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jul 02 17:44:13 2002 +0200
@@ -583,7 +583,8 @@
val thms_containingP =
OuterSyntax.improper_command "thms_containing"
"print facts containing certain constants or variables"
- K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+ K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
+ Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
val thm_depsP =
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"