# HG changeset patch # User wenzelm # Date 1408699731 -7200 # Node ID c6b131e651e68892754b6be1cf9dddcf12c6f50b # Parent 2137e60b6f6d0cdb54fa78ac2deefbd2065404a6 made SML/NJ happy; diff -r 2137e60b6f6d -r c6b131e651e6 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Aug 21 23:54:27 2014 +0200 +++ b/src/Pure/Isar/method.ML Fri Aug 22 11:28:51 2014 +0200 @@ -87,8 +87,8 @@ type method = thm list -> cases_tactic; -fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); -fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); +fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); +fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); val fail = METHOD (K no_tac); val succeed = METHOD (K all_tac);