# HG changeset patch
# User wenzelm
# Date 1138144895 -3600
# Node ID 9d98d5705433a2296315bbbb624a024c7cf5435a
# Parent  fdc5379fd359eee041dd85ae02bbca5fdacc7761
abs_def: improved error;

diff -r fdc5379fd359 -r 9d98d5705433 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jan 25 00:21:34 2006 +0100
+++ b/src/Pure/drule.ML	Wed Jan 25 00:21:35 2006 +0100
@@ -725,8 +725,9 @@
   let
     fun contract_lhs th =
       Thm.transitive (Thm.symmetric (beta_eta_conversion (fst (dest_equals (cprop_of th))))) th;
-    fun abstract cx = Thm.abstract_rule
-      (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx;
+    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 dest_equals o cprop_of)