--- a/src/Pure/Isar/isar_syn.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML Fri Feb 13 07:53:38 2009 +1100
@@ -878,6 +878,22 @@
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));