changeset 56254 | a2dd9200854d |
parent 56220 | 4c43a2881b25 |
child 58634 | 9f10d82e8188 |
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 18:16:54 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 18:19:57 2014 +0100 @@ -1053,7 +1053,7 @@ (Object_Logic.atomize_term thy prop) val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl)) |> map_types (map_type_tfree - (fn (s, []) => TFree (s, HOLogic.typeS) + (fn (s, []) => TFree (s, @{sort type}) | x => TFree x)) val _ = if debug then