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)