# HG changeset patch
# User wenzelm
# Date 1389479705 -3600
# Node ID 68228c162ed547dbeb209d0583ec6758a6a60e0e
# Parent  8e98d67325b125f9fade9c8a56d77e0d878db826
more accurate context;

diff -r 8e98d67325b1 -r 68228c162ed5 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sat Jan 11 21:39:21 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sat Jan 11 23:35:05 2014 +0100
@@ -103,7 +103,8 @@
         Drule.cterm_instantiate subst relcomppI
       end
 
-    fun zip_transfer_rules ctxt thm =       let
+    fun zip_transfer_rules ctxt thm =
+      let
         val thy = Proof_Context.theory_of ctxt
         fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
         val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
@@ -122,7 +123,8 @@
     val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
     val assms = cprems_of fixed_thm
     val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
-    val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
+    val (prems, ctxt) = fold_map Thm.assume_hyps assms ctxt
+    val ctxt = Context.proof_map (fold add_transfer_rule prems) ctxt
     val zipped_thm =
       fixed_thm
       |> undisch_all