# HG changeset patch
# User huffman
# Date 1333518462 -7200
# Node ID 600e6b07a69361841af8ab649f08d0f7bdef43cd
# Parent  b4490e1a07323eb926b8810dabea60aecdb3d6bc
add type annotations to make SML happy (cf. ec6187036495)

diff -r b4490e1a0732 -r 600e6b07a693 src/HOL/Tools/transfer.ML
--- 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 *)