# HG changeset patch
# User huffman
# Date 1335539653 -7200
# Node ID 2e3821e13d677b4c12b888ce02da81c059110748
# Parent  f6cf7148d45284443979de9eb23139439b013919
allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing

diff -r f6cf7148d452 -r 2e3821e13d67 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Fri Apr 27 17:06:36 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Fri Apr 27 17:14:13 2012 +0200
@@ -10,6 +10,7 @@
   val get_relator_eq: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
+  val transfer_rule_of_term: Proof.context -> term -> thm
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
@@ -193,6 +194,8 @@
     val start_rule = 
       if equiv then @{thm transfer_start} else @{thm transfer_start'}
     val rules = Data.get ctxt
+    (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
+    val end_tac = if equiv then K all_tac else K no_tac
   in
     EVERY
       [rewrite_goal_tac pre_simps i THEN
@@ -201,7 +204,7 @@
          (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
            THEN_ALL_NEW
              (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
-               ORELSE' eq_tac ctxt)) (i + 1)) i,
+               ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
        rtac @{thm _} i]