src/Pure/variable.ML

--- a/src/Pure/variable.ML	Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/variable.ML	Fri Mar 06 17:32:20 2015 +0100
@@ -587,9 +587,8 @@
 
 fun focus_cterm goal ctxt =
   let
-    val thy = Thm.theory_of_cterm goal;
     val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
-    val ps' = map (Thm.global_cterm_of thy o Free) ps;
+    val ps' = map (Thm.cterm_of ctxt' o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
   in ((xs ~~ ps', goal'), ctxt') end;