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