# HG changeset patch
# User urbanc
# Date 1133064583 -3600
# Node ID f3f81becc1f16feba979f9e30260557422ad8384
# Parent  3b808e24667b8b4e08f6ba12c95f7ade75d1b33d
some minor tunings

diff -r 3b808e24667b -r f3f81becc1f1 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;