src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 41870 a14a492f472f
parent 41860 49d0fc8c418c
child 41875 e3cd0dce9b1a
equal deleted inserted replaced
41869:9e367f1c9570 41870:a14a492f472f
  1282       #> Term.map_abs_vars shortest_name
  1282       #> Term.map_abs_vars shortest_name
  1283     val nondef_ts = nondef_ts |> map (do_middle false)
  1283     val nondef_ts = nondef_ts |> map (do_middle false)
  1284     val preconstr_ts =
  1284     val preconstr_ts =
  1285       (* FIXME: Implement preconstruction inference. *)
  1285       (* FIXME: Implement preconstruction inference. *)
  1286       preconstrs
  1286       preconstrs
  1287       |> map_filter (fn (SOME t, SOME true) => SOME (t |> do_middle false)
  1287       |> map_filter (fn (SOME t, SOME true) =>
       
  1288                         SOME (t |> unfold_defs_in_term hol_ctxt
       
  1289                                 |> do_middle false)
  1288                       | _ => NONE)
  1290                       | _ => NONE)
  1289     val nondef_ts = nondef_ts |> map (do_tail false)
  1291     val nondef_ts = nondef_ts |> map (do_tail false)
  1290     val def_ts = def_ts |> map (do_middle true #> do_tail true)
  1292     val def_ts = def_ts |> map (do_middle true #> do_tail true)
  1291   in
  1293   in
  1292     (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
  1294     (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,