src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 59970 e9f73d87d904
parent 59621 291934bac95e
child 60139 9fabfda0643f
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -1050,7 +1050,7 @@
     1.4      fun try_out negate =
     1.5        let
     1.6          val concl = (negate ? curry (op $) @{const Not})
     1.7 -                    (Object_Logic.atomize_term thy prop)
     1.8 +                    (Object_Logic.atomize_term ctxt prop)
     1.9          val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
    1.10                     |> map_types (map_type_tfree
    1.11                                       (fn (s, []) => TFree (s, @{sort type})
    1.12 @@ -1062,7 +1062,7 @@
    1.13              |> writeln
    1.14            else
    1.15              ()
    1.16 -        val goal = prop |> Thm.global_cterm_of thy |> Goal.init
    1.17 +        val goal = prop |> Thm.cterm_of ctxt |> Goal.init
    1.18        in
    1.19          (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
    1.20                |> the |> Goal.finish ctxt; true)