changeset 57954 | c52223cd1003 |
parent 57945 | cacb00a569e0 |
child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/Cfun.thy Sat Aug 16 14:42:35 2014 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Sat Aug 16 16:18:39 2014 +0200 @@ -148,7 +148,7 @@ val tr = instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2}); val rules = Named_Theorems.get ctxt @{named_theorems cont2cont}; - val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)); + val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules))); in SOME (perhaps (SINGLE (tac 1)) tr) end *}