Added error messages.
authornipkow
Fri Oct 17 15:23:14 1997 +0200 (1997-10-17)
changeset 391894e0fdcb7b91
parent 3917 6ea5f9101c3e
child 3919 c036caebfc75
Added error messages.
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Fri Oct 17 11:12:36 1997 +0200
     1.2 +++ b/src/Provers/splitter.ML	Fri Oct 17 15:23:14 1997 +0200
     1.3 @@ -257,9 +257,12 @@
     1.4  
     1.5  fun split_tac [] i = no_tac
     1.6    | split_tac splits i =
     1.7 -  let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
     1.8 -                           val (Const(a,_),args) = strip_comb lhs
     1.9 -                       in (a,(thm,fastype_of t,length args)) end
    1.10 +  let fun const(thm) =
    1.11 +            (case concl_of thm of _$(t as _$lhs)$_ =>
    1.12 +               (case strip_comb lhs of (Const(a,_),args) =>
    1.13 +                  (a,(thm,fastype_of t,length args))
    1.14 +                | _ => error("Wrong format for split rule"))
    1.15 +             | _ => error("Wrong format for split rule"))
    1.16        val cmap = map const splits;
    1.17        fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
    1.18        fun lift_split_tac st = st |>