src/Pure/drule.ML
changeset 24947 b7e990e1706a
parent 24848 5dbbd33c3236
child 24978 159b0f4dd1e9
--- 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 ***)