changeset 31794 | 71af1fd6a5e4 |
parent 30552 | 58db56278478 |
child 32200 | 2bd8ab91a426 |
--- a/src/Pure/subgoal.ML Wed Jun 24 20:52:49 2009 +0200 +++ b/src/Pure/subgoal.ML Wed Jun 24 21:28:02 2009 +0200 @@ -29,7 +29,7 @@ fun focus ctxt i st = let val ((schematics, [st']), ctxt') = - Variable.import_thms true [Simplifier.norm_hhf_protect st] ctxt; + Variable.import true [Simplifier.norm_hhf_protect st] ctxt; val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt'; val asms = Drule.strip_imp_prems goal; val concl = Drule.strip_imp_concl goal;