Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
abs_def: improved error;
authorwenzelm
Wed, 25 Jan 2006 00:21:35 +0100
changeset 18777 9d98d5705433
parent 18776 fdc5379fd359
child 18778 f623f7a35ced
abs_def: improved error;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle