src/HOL/simpdata.ML
changeset 3577 9715b6e3ec5f
parent 3573 7544c866315c
child 3615 e5322197cfea
     1.1 --- a/src/HOL/simpdata.ML	Fri Jul 25 13:17:14 1997 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jul 25 13:18:09 1997 +0200
     1.3 @@ -170,14 +170,14 @@
     1.4                   rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
     1.5    in rule_by_tactic tac (trivial ceqt) end;
     1.6  
     1.7 -fun rearrange sg (F as ex $ Abs(x,T,P)) =
     1.8 +fun rearrange sg _ (F as ex $ Abs(x,T,P)) =
     1.9       (case extract P of
    1.10          None => None
    1.11        | Some(eq,Q) =>
    1.12            let val ceqt = cterm_of sg
    1.13                         (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
    1.14            in Some(prove_eq ceqt) end)
    1.15 -  | rearrange _ _ = None;
    1.16 +  | rearrange _ _ _ = None;
    1.17  
    1.18  val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
    1.19