changeset 59498 | 50b60f501b05 |
parent 58963 | 26bf09b95dda |
child 60754 | 02924903a6fd |
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Feb 10 14:48:26 2015 +0100 @@ -105,7 +105,7 @@ SELECT_GOAL (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1), - REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), + REPEAT (resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), rtac @{thm ns_constrainsI} 1, full_simp_tac ctxt 1, REPEAT (FIRSTGOAL (etac disjE)),