Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made SML/NJ happy;
authorwenzelm
Fri, 22 Aug 2014 11:28:51 +0200
changeset 58030 c6b131e651e6
parent 58029 2137e60b6f6d
child 58031 b2b93903ab6b
made SML/NJ happy;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle