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