author | huffman |
Thu, 05 Nov 2009 15:38:09 -0800 | |
changeset 33505 | 03221db9df29 |
parent 33504 | b4210cc3ac97 |
child 33506 | afb577487b15 |
--- a/src/HOLCF/Tools/fixrec.ML Thu Nov 05 11:47:00 2009 -0800 +++ b/src/HOLCF/Tools/fixrec.ML Thu Nov 05 15:38:09 2009 -0800 @@ -391,7 +391,7 @@ CHANGED (rtac rule i THEN asm_simp_tac ss i) end in - SUBGOAL (fn ti => tac ti handle _ => no_tac) + SUBGOAL (fn ti => the_default no_tac (try tac ti)) end; val fixrec_simp_add : Thm.attribute =