# HG changeset patch
# User huffman
# Date 1333548352 -7200
# Node ID 19fb95255ec9ff1d8c7be99d792766a0e18a3ac9
# Parent  3d9d98e0f1a418b503905e1c884647f52631acb2
transfer method generalizes over free variables in goal

diff -r 3d9d98e0f1a4 -r 19fb95255ec9 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Apr 04 16:03:01 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Apr 04 16:05:52 2012 +0200
@@ -117,6 +117,14 @@
   @{thms App_def Abs_def transfer_forall_eq [symmetric]
     transfer_implies_eq [symmetric] transfer_bforall_unfold}
 
+fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
+  let
+    val vs = rev (Term.add_frees t [])
+    val vs' = filter_out (member (op =) keepers o fst) vs
+  in
+    Induct.arbitrary_tac ctxt 0 vs' i
+  end)
+
 fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
   let
     val bs = bnames t
@@ -147,7 +155,7 @@
   end
 
 val transfer_method : (Proof.context -> Method.method) context_parser =
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (gen_frees_tac [] ctxt THEN' transfer_tac ctxt))
 
 val correspondence_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))