# HG changeset patch
# User wenzelm
# Date 952639000 -3600
# Node ID 64921d1fef1562be4abdfcd0b1d20f0a3072e456
# Parent  86b04d47b8535ffad4b9632a906855985347f90e
cleaned comment;

diff -r 86b04d47b853 -r 64921d1fef15 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Thu Mar 09 18:27:18 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Thu Mar 09 22:56:40 2000 +0100
@@ -213,7 +213,7 @@
 
     val rules =
       (case (args, facts) of
-        ((None, None), []) => [RuleCases.none case_split_thm]
+        ((None, None), []) => [RuleCases.none case_split_thm]		(* FIXME add cases!? *)
       | ((Some t, None), []) =>
           let val name = type_name t in
             (case lookup_casesT ctxt name of
diff -r 86b04d47b853 -r 64921d1fef15 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Mar 09 18:27:18 2000 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 09 22:56:40 2000 +0100
@@ -3,9 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Manage local contexts of rules.
-
-TODO:
-  - instantiation of cases (including type vars!);
 *)
 
 signature RULE_CASES =