| changeset 26291 | d01bf7b10c75 |
| parent 25985 | 8d69087f6a4b |
| child 26568 | 3a3a83493f00 |
--- a/src/Tools/induct.ML Sat Mar 15 22:07:31 2008 +0100 +++ b/src/Tools/induct.ML Sat Mar 15 22:07:32 2008 +0100 @@ -309,7 +309,7 @@ RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); fun warn_open true = - legacy_feature ("open rule cases in proof method" ^ Position.str_of (Position.thread_data ())) + legacy_feature ("Open rule cases in proof method" ^ Position.str_of (Position.thread_data ())) | warn_open false = ();