# HG changeset patch
# User krauss
# Date 1170687332 -3600
# Node ID 264eabb113d32e1c909c8d8fd311fa87360f1e56
# Parent  0f24888c8591408ed4fe1e6867354be6c0f44997
Exporting curried versions of tail recursive equations instead of internal ones

diff -r 0f24888c8591 -r 264eabb113d3 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Mon Feb 05 12:03:52 2007 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Mon Feb 05 15:55:32 2007 +0100
@@ -366,7 +366,7 @@
                      psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
                      cases=expand cases, termination=expand mtermination,
                      domintros=map_option (map expand) domintros,
-                     trsimps=map_option (map expand) trsimps}
+                     trsimps=map_option (map expand) mtrsimps}
     end