src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33747 3aa6b9911252
parent 33743 a58893035742
child 33851 ab6ecae44033
equal deleted inserted replaced
33746:6c6ce0757bfe 33747:3aa6b9911252
  1414 fun is_constr_pattern_formula thy t =
  1414 fun is_constr_pattern_formula thy t =
  1415   case lhs_of_equation t of
  1415   case lhs_of_equation t of
  1416     SOME t' => is_constr_pattern_lhs thy t'
  1416     SOME t' => is_constr_pattern_lhs thy t'
  1417   | NONE => false
  1417   | NONE => false
  1418 
  1418 
  1419 val unfold_max_depth = 63
  1419 val unfold_max_depth = 255
  1420 val axioms_max_depth = 63
  1420 val axioms_max_depth = 255
  1421 
  1421 
  1422 (* extended_context -> term -> term *)
  1422 (* extended_context -> term -> term *)
  1423 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
  1423 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
  1424                                       case_names, def_table, ground_thm_table,
  1424                                       case_names, def_table, ground_thm_table,
  1425                                       ersatz_table, ...}) =
  1425                                       ersatz_table, ...}) =