src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 35665 ff2bf50505ab
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -807,7 +807,7 @@
     1.4      fun try_out negate =
     1.5        let
     1.6          val concl = (negate ? curry (op $) @{const Not})
     1.7 -                    (ObjectLogic.atomize_term thy prop)
     1.8 +                    (Object_Logic.atomize_term thy 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, HOLogic.typeS)