changeset 60801 | 7664e0916eec |
parent 60754 | 02924903a6fd |
child 61144 | 5e94dfead1c2 |
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jul 27 17:44:55 2015 +0200 @@ -121,7 +121,7 @@ local fun solve_cont ctxt t = let - val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} + val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end in fun cont_proc thy =