# HG changeset patch
# User krauss
# Date 1183466907 -7200
# Node ID 55597852285a4c8f570915cbb142dc4013994111
# Parent  c1d2fa4b76dfe010e7e9ff65d749592632cb8f7c
fixed an issue with mutual recursion

diff -r c1d2fa4b76df -r 55597852285a src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Jul 03 01:26:06 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Jul 03 14:48:27 2007 +0200
@@ -34,6 +34,9 @@
 val projl_inl = thm "Sum_Type.Projl_Inl"
 val projr_inr = thm "Sum_Type.Projr_Inr"
 
+(* top-down access in balanced tree *)
+fun access_top_down {left, right, init} len i =
+    BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
@@ -42,17 +45,17 @@
 val App = curry op $
 
 fun mk_inj ST n i = 
-    BalancedTree.access 
+    access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, App (Const (@{const_name "Inl"}, LT --> T)) o inj)),
-      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, App (Const (@{const_name "Inr"}, RT --> T)) o inj))} n i 
+      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
+      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i 
     |> snd
 
 fun mk_proj ST n i = 
-    BalancedTree.access 
+    access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, proj o App (Const (@{const_name "Projl"}, T --> LT)))),
-      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, proj o App (Const (@{const_name "Projr"}, T --> RT))))} n i
+      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Projl"}, T --> LT)) o proj)),
+      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Projr"}, T --> RT)) o proj))} n i
     |> snd
 
 fun mk_sumcases T fs =