changeset 59582 | 0fbed69ff081 |
parent 59058 | a78612c67ec0 |
child 59621 | 291934bac95e |
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Mar 04 19:53:18 2015 +0100 @@ -1062,7 +1062,7 @@ |> writeln else () - val goal = prop |> cterm_of thy |> Goal.init + val goal = prop |> Thm.cterm_of thy |> Goal.init in (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt)) |> the |> Goal.finish ctxt; true)