--- a/src/Tools/induct_tacs.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/induct_tacs.ML Sun Nov 01 15:24:45 2009 +0100
@@ -86,9 +86,9 @@
val argss = map (map (Option.map induct_var)) varss;
val rule =
(case opt_rules of
- SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
+ SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
| NONE =>
- (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
+ (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
(_, rule) :: _ => rule
| [] => raise THM ("No induction rules", 0, [])));