# HG changeset patch
# User krauss
# Date 1150807919 -7200
# Node ID baeb0aeb489105a0e3d1f20b5f83a3794c412523
# Parent  5c882c3e610b15eeadfcf7cb102484811ea98f5a
Fixed another variable order bug...

diff -r 5c882c3e610b -r baeb0aeb4891 src/HOL/Tools/function_package/fundef_proof.ML
--- 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)]