changeset 39345 | 062c10ff848c |
parent 38864 | 4abe644fcea5 |
child 39359 | 6f49c7fbb1b1 |
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Sep 13 20:21:24 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Sep 13 20:21:40 2010 +0200 @@ -982,7 +982,7 @@ else if s = @{const_name TYPE} then accum else case def_of_const thy def_table x of - SOME def => + SOME _ => fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) accum | NONE =>