1.1 --- a/src/HOL/Tools/Function/function.ML	Wed Jan 20 14:05:17 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Wed Jan 20 14:09:46 2010 +0100
     1.3 @@ -164,6 +164,7 @@
     1.4                simps=SOME simps, inducts=SOME inducts, termination=termination }
     1.5              in
     1.6                Local_Theory.declaration false (add_function_data o morph_function_data info')
     1.7 +              #> Spec_Rules.add Spec_Rules.Equational (fs, simps)
     1.8              end)
     1.9          end
    1.10    in