# HG changeset patch # User huffman # Date 1334763879 -7200 # Node ID 98c8b7542b72594521984d1f16e5c22de15097a7 # Parent 407cabf66f2166a771ece9f9b1f82a61e1e897c3 add option to transfer method for specifying variables not to generalize over diff -r 407cabf66f21 -r 98c8b7542b72 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Tue Apr 17 16:21:47 2012 +1000 +++ b/src/HOL/Tools/transfer.ML Wed Apr 18 17:44:39 2012 +0200 @@ -130,7 +130,7 @@ 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 + val vs' = filter_out (member (op =) keepers) vs in Induct.arbitrary_tac ctxt 0 vs' i end) @@ -167,8 +167,15 @@ (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i] end +val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => + error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) + +val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) + |-- Scan.repeat free) [] + val transfer_method : (Proof.context -> Method.method) context_parser = - Scan.succeed (fn ctxt => SIMPLE_METHOD' (gen_frees_tac [] ctxt THEN' transfer_tac ctxt)) + fixing >> (fn vs => fn ctxt => + SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac ctxt)) val correspondence_method : (Proof.context -> Method.method) context_parser = Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))