src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 41870 a14a492f472f
parent 41860 49d0fc8c418c
child 41875 e3cd0dce9b1a
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Mar 02 13:09:57 2011 +0100
@@ -1284,7 +1284,9 @@
     val preconstr_ts =
       (* FIXME: Implement preconstruction inference. *)
       preconstrs
-      |> map_filter (fn (SOME t, SOME true) => SOME (t |> do_middle false)
+      |> map_filter (fn (SOME t, SOME true) =>
+                        SOME (t |> unfold_defs_in_term hol_ctxt
+                                |> do_middle false)
                       | _ => NONE)
     val nondef_ts = nondef_ts |> map (do_tail false)
     val def_ts = def_ts |> map (do_middle true #> do_tail true)