| changeset 22826 | 0f4c501a691e |
| parent 21879 | a3efbae45735 |
| child 22900 | f8a7c10e1bd0 |
--- a/src/Provers/induct_method.ML Mon Apr 30 13:22:35 2007 +0200 +++ b/src/Provers/induct_method.ML Mon Apr 30 13:32:58 2007 +0200 @@ -95,7 +95,7 @@ fun make_cases is_open rule = RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); -fun warn_open true = warning "Encountered open rule cases -- deprecated" +fun warn_open true = legacy_feature "open rule cases in proof method" | warn_open false = ();