# HG changeset patch
# User wenzelm
# Date 1140110755 -3600
# Node ID fdffd7c408649cdacb41008b5cd71ffc37c612ff
# Parent  99001616e0e29771d44c703c3660a57105cf7178
dest_def: actually return beta-eta contracted equation;

diff -r 99001616e0e2 -r fdffd7c40864 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Feb 16 18:25:54 2006 +0100
+++ b/src/Pure/logic.ML	Thu Feb 16 18:25:55 2006 +0100
@@ -206,13 +206,15 @@
 fun dest_def pp check_head is_fixed is_fixedT eq =
   let
     fun err msg = raise TERM (msg, [eq]);
-    val bound_vars = Syntax.bound_vars (Term.strip_all_vars eq);
-    val display_terms = commas_quote o map (Pretty.string_of_term pp o bound_vars);
+    val eq_vars = Term.strip_all_vars eq;
+    val eq_body = Term.strip_all_body eq;
+
+    val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
     val display_types = commas_quote o map (Pretty.string_of_typ pp);
 
-    val (lhs, rhs) = dest_equals (Term.strip_all_body eq)
-      handle TERM _ => err "Not a meta-equality (==)";
-    val (head, args) = Term.strip_comb (Envir.beta_eta_contract lhs);
+    val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
+    val lhs = Envir.beta_eta_contract raw_lhs;
+    val (head, args) = Term.strip_comb lhs;
     val head_tfrees = Term.add_tfrees head [];
 
     fun check_arg (Bound _) = true
@@ -243,7 +245,7 @@
       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
     else if exists_subterm (fn t => t aconv head) rhs then
       err "Entity to be defined occurs on rhs"
-    else ((lhs, rhs), fold_rev close_arg args eq)
+    else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
   end;
 
 (*!!x. c x == t[x] to c == %x. t[x]*)