src/HOL/Nominal/nominal_induct.ML

--- a/src/HOL/Nominal/nominal_induct.ML	Sun Nov 27 05:00:43 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 27 05:09:43 2005 +0100
@@ -83,12 +83,5 @@
 val nominal_induct_method =
   Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
 
-(* nominal_induc_method needs to have the type
-
-   Args.src -> Proof.context -> Proof.method
-
-   CHECK THAT
-
-*)
 
 end;