src/Pure/subgoal.ML

--- a/src/Pure/subgoal.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/subgoal.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -31,7 +31,7 @@
 
 fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val st = Simplifier.norm_hhf_protect raw_st;
+    val st = Simplifier.norm_hhf_protect ctxt raw_st;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;