src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -1062,7 +1062,7 @@
     1.4              |> writeln
     1.5            else
     1.6              ()
     1.7 -        val goal = prop |> Thm.cterm_of thy |> Goal.init
     1.8 +        val goal = prop |> Thm.global_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)