changeset 59498 | 50b60f501b05 |
parent 58963 | 26bf09b95dda |
child 59582 | 0fbed69ff081 |
--- a/src/Doc/Isar_Ref/Generic.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Tue Feb 10 14:48:26 2015 +0100 @@ -1054,7 +1054,7 @@ ML \<open> fun subgoaler_tac ctxt = assume_tac ctxt ORELSE' - resolve_tac (Simplifier.prems_of ctxt) ORELSE' + resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE' asm_simp_tac ctxt \<close>