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.
add type annotations to make SML happy (cf. ec6187036495)
authorhuffman
Wed, 04 Apr 2012 07:47:42 +0200
changeset 47327 600e6b07a693
parent 47326 b4490e1a0732
child 47328 9f11a3cd84b1
add type annotations to make SML happy (cf. ec6187036495)
src/HOL/Tools/transfer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/transfer.ML	Tue Apr 03 23:49:24 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Apr 04 07:47:42 2012 +0200
@@ -143,10 +143,10 @@
          (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
   end
 
-val transfer_method =
+val transfer_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
 
-val correspondence_method =
+val correspondence_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
 
 (* Attribute for correspondence rules *)
isabelle