src/HOL/Tools/inductive.ML
changeset 54883 dd04a8b654fc
parent 54742 7a86358a3c0b
child 55111 5792f5106c40
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Dec 31 11:19:14 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Tue Dec 31 14:29:16 2013 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4    hol_simplify ctxt inductive_conj
     1.5    #> hol_simplify ctxt inductive_rulify
     1.6    #> hol_simplify ctxt inductive_rulify_fallback
     1.7 -  #> Simplifier.norm_hhf;
     1.8 +  #> Simplifier.norm_hhf ctxt;
     1.9  
    1.10  end;
    1.11