# HG changeset patch
# User krauss
# Date 1158240305 -7200
# Node ID b147d0c13f6eed0f45cb5d71f24e2015cd2afb4a
# Parent  49442b3024bb012c1b59efd052a3e01e985e7b7f
Fixed Subscript Exception occurring with Higher-Order recursion

diff -r 49442b3024bb -r b147d0c13f6e src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Thu Sep 14 03:25:17 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Thu Sep 14 15:25:05 2006 +0200
@@ -65,8 +65,9 @@
       val (fc, args) = strip_comb f_args
       val f as (fname, _) = check_head fnames fc
 
-      val add_bvs = fold_aterms (fn Bound i => insert (op =) i | _ => I)
+      fun add_bvs t is = add_loose_bnos (t, 0, is)
       val rhs_only = (add_bvs rhs [] \\ fold add_bvs args [])
+                       |> print
                         |> map (fst o nth (rev qs))
       val _ = if null rhs_only then () 
 	      else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *)