# HG changeset patch
# User wenzelm
# Date 1192030314 -7200
# Node ID b7e990e1706a0c0b02dff200505caa50b75ddc54
# Parent  a7bcad4137998a9ada62c3277b21ad485222896d
improved abs_def: only abstract over outermost (unique) Vars;

diff -r a7bcad413799 -r b7e990e1706a src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Oct 10 17:31:53 2007 +0200
+++ b/src/Pure/drule.ML	Wed Oct 10 17:31:54 2007 +0200
@@ -602,20 +602,39 @@
 fun eta_contraction_rule th =
   equal_elim (eta_conversion (cprop_of th)) th;
 
-val abs_def =
+
+(* abs_def *)
+
+(*
+   f ?x1 ... ?xn == u
+  --------------------
+   f == %x1 ... xn. u
+*)
+
+local
+
+fun contract_lhs th =
+  Thm.transitive (Thm.symmetric (beta_eta_conversion
+    (fst (Thm.dest_equals (cprop_of th))))) th;
+
+fun var_args ct =
+  (case try Thm.dest_comb ct of
+    SOME (f, arg) =>
+      (case Thm.term_of arg of
+        Var ((x, _), _) => update (eq_snd (op aconvc)) (x, arg) (var_args f)
+      | _ => [])
+  | NONE => []);
+
+in
+
+fun abs_def th =
   let
-    fun contract_lhs th =
-      Thm.transitive (Thm.symmetric (beta_eta_conversion
-        (fst (Thm.dest_equals (cprop_of th))))) th;
-    fun abstract cx th = Thm.abstract_rule
-        (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx th
-      handle THM _ => raise THM ("Malformed definitional equation", 0, [th]);
-  in
-    contract_lhs
-    #> `(snd o strip_comb o fst o Thm.dest_equals o cprop_of)
-    #-> fold_rev abstract
-    #> contract_lhs
-  end;
+    val th' = contract_lhs th;
+    val args = var_args (Thm.lhs_of th');
+  in contract_lhs (fold (uncurry Thm.abstract_rule) args th') end;
+
+end;
+
 
 
 (*** Some useful meta-theorems ***)