changeset 58839 | ccda99401bc8 |
parent 58634 | 9f10d82e8188 |
child 59498 | 50b60f501b05 |
--- a/src/HOL/Tools/Function/function_lib.ML Thu Oct 30 16:55:29 2014 +0100 +++ b/src/HOL/Tools/Function/function_lib.ML Thu Oct 30 22:45:19 2014 +0100 @@ -113,7 +113,7 @@ then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) (K (rewrite_goals_tac ctxt ac - THEN rtac Drule.reflexive_thm 1)) + THEN resolve_tac [Drule.reflexive_thm] 1)) end (* instance for unions *)