src/Pure/drule.ML
changeset 18777 9d98d5705433
parent 18732 c0511e120f17
child 18799 f137c5e971f5
     1.1 --- a/src/Pure/drule.ML	Wed Jan 25 00:21:34 2006 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Jan 25 00:21:35 2006 +0100
     1.3 @@ -725,8 +725,9 @@
     1.4    let
     1.5      fun contract_lhs th =
     1.6        Thm.transitive (Thm.symmetric (beta_eta_conversion (fst (dest_equals (cprop_of th))))) th;
     1.7 -    fun abstract cx = Thm.abstract_rule
     1.8 -      (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx;
     1.9 +    fun abstract cx th = Thm.abstract_rule
    1.10 +        (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx th
    1.11 +      handle THM _ => raise THM ("Malformed definitional equation", 0, [th]);
    1.12    in
    1.13      contract_lhs
    1.14      #> `(snd o strip_comb o fst o dest_equals o cprop_of)