author | huffman |
Thu, 15 Jan 2009 14:33:38 -0800 | |
changeset 29541 | 35c2654a95da |
parent 29540 | 8858d197a9b6 |
child 29542 | d20f453eb4a3 |
--- a/src/HOLCF/Cont.thy Thu Jan 15 12:43:41 2009 -0800 +++ b/src/HOLCF/Cont.thy Thu Jan 15 14:33:38 2009 -0800 @@ -159,7 +159,7 @@ let val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI; val rules = Cont2ContData.get (Simplifier.the_context ss); - val tac = REPEAT_ALL_NEW (resolve_tac rules); + val tac = REPEAT_ALL_NEW (match_tac rules); in Option.map fst (Seq.pull (tac 1 tr)) end val proc =