| changeset 54883 | dd04a8b654fc |
| parent 54742 | 7a86358a3c0b |
| child 55111 | 5792f5106c40 |
--- a/src/HOL/Tools/inductive.ML Tue Dec 31 11:19:14 2013 +0100 +++ b/src/HOL/Tools/inductive.ML Tue Dec 31 14:29:16 2013 +0100 @@ -357,7 +357,7 @@ hol_simplify ctxt inductive_conj #> hol_simplify ctxt inductive_rulify #> hol_simplify ctxt inductive_rulify_fallback - #> Simplifier.norm_hhf; + #> Simplifier.norm_hhf ctxt; end;