src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -935,7 +935,7 @@
 
 fun comp_hhf_tac ctxt th i st =
   PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
-    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+    (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
 
 fun comp_incr_tac _ [] _ = no_tac
   | comp_incr_tac ctxt (th :: ths) i =