# HG changeset patch
# User nipkow
# Date 877094594 -7200
# Node ID 94e0fdcb7b91c691dd543b4a0550402d47b3fdee
# Parent  6ea5f9101c3e84ddafefb515bc4bc3e873edc160
Added error messages.

diff -r 6ea5f9101c3e -r 94e0fdcb7b91 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Oct 17 11:12:36 1997 +0200
+++ b/src/Provers/splitter.ML	Fri Oct 17 15:23:14 1997 +0200
@@ -257,9 +257,12 @@
 
 fun split_tac [] i = no_tac
   | split_tac splits i =
-  let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
-                           val (Const(a,_),args) = strip_comb lhs
-                       in (a,(thm,fastype_of t,length args)) end
+  let fun const(thm) =
+            (case concl_of thm of _$(t as _$lhs)$_ =>
+               (case strip_comb lhs of (Const(a,_),args) =>
+                  (a,(thm,fastype_of t,length args))
+                | _ => error("Wrong format for split rule"))
+             | _ => error("Wrong format for split rule"))
       val cmap = map const splits;
       fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
       fun lift_split_tac st = st |>