changeset 60695 | 757549b4bbe6 |
parent 59621 | 291934bac95e |
child 60781 | 2da59cdf531c |
--- a/src/HOL/Tools/Function/function_context_tree.ML Wed Jul 08 15:37:32 2015 +0200 +++ b/src/HOL/Tools/Function/function_context_tree.ML Wed Jul 08 19:28:43 2015 +0200 @@ -103,7 +103,7 @@ (* Called on the INSTANTIATED branches of the congruence rule *) fun mk_branch ctxt t = let - val ((params, impl), ctxt') = Variable.focus t ctxt + val ((params, impl), ctxt') = Variable.focus NONE t ctxt val (assms, concl) = Logic.strip_horn impl in (ctxt', map #2 params, assms, rhs_of concl)