Fixed another variable order bug...

--- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 20 10:16:22 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 20 14:51:59 2006 +0200
@@ -398,11 +398,15 @@
 
 		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
 
-		val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)
+		val z_acc' = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject))
+                               |> FundefCtxTree.export_thm thy ([], (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
+
+                val occvars = fold (OrdList.insert Term.term_ord) (term_frees (prop_of z_acc')) [] 
+                val ordvars = fold (OrdList.insert Term.term_ord) (map Free fixes @ qs) [] (* FIXME... remove when inductive behaves nice *)
+                                   |> OrdList.inter Term.term_ord occvars
 
 		val ethm = z_acc'
-			       |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
-			       |> fold_rev forall_intr cqs
+			       |> FundefCtxTree.export_thm thy (map dest_Free ordvars, [])
 
 
 		val sub' = sub @ [(([],[]), acc)]