# HG changeset patch
# User wenzelm
# Date 1376681285 -7200
# Node ID aa0322a65bea5f378c2823058db6179cc5c02f2f
# Parent  d51bac27d4a0ad86aaddfffb3118a13fdcd6b404
standardized aliases;

diff -r d51bac27d4a0 -r aa0322a65bea src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Fri Aug 16 20:58:15 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Fri Aug 16 21:28:05 2013 +0200
@@ -666,11 +666,11 @@
 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
   |-- Scan.repeat free) []
 
-fun transfer_method equiv : (Proof.context -> Method.method) context_parser =
+fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
   fixing >> (fn vs => fn ctxt =>
     SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
 
-val transfer_prover_method : (Proof.context -> Method.method) context_parser =
+val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
 
 (* Attribute for transfer rules *)