src/Provers/splitter.ML

       iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
 
 *)
 
 local
+
+fun split_format_err() = error("Wrong format for split rule");
 
 fun mk_case_split_tac_2 iffD order =
 let
 
 

       val abss = foldl (fn (t, T) => Abs ("", T, t))
   in
     term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm)
   end;
 
-
 (*****************************************************************************
    The split-tactic
    
    splits : list of split-theorems to be tried
    i      : number of subgoal the tactic should be applied to

   | split_tac splits i =
   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"))
+                | _ => split_format_err())
+             | _ => split_format_err())
       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 |>
             let val (Ts,t,splits) = select cmap st i
             in case splits of

           (rtac iffD i THEN lift_split_tac)
   end;
 
 in split_tac end;
 
+(* FIXME: this junk is only HOL specific and should therefore not go here! *)
+(* const_of_split_thm is used in HOL/simpdata.ML *)
+
+fun const_of_split_thm thm =
+  (case concl_of thm of
+     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$_) =>
+        (case strip_comb t of
+           (Const(a,_),_) => a
+         | _              => split_format_err())
+   | _ => split_format_err());
 
 fun mk_case_split_asm_tac split_tac 
 			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
 let
 

    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
 fun split_asm_tac []     = K no_tac
   | split_asm_tac splits = 
-  let fun const thm =
-            (case concl_of thm of Const ("Trueprop",_)$
-				 (Const ("op =", _)$(Var _$t)$_) =>
-               (case strip_comb t of (Const(a,_),_) => a
-                | _ => error("Wrong format for split rule"))
-             | _ =>    error("Wrong format for split rule"))
-      val cname_list = map const splits;
+  let val cname_list = map const_of_split_thm splits;
       fun is_case (a,_) = a mem cname_list;
       fun tac (t,i) = 
 	  let val n = find_index (exists_Const is_case) 
 				 (Logic.strip_assums_hyp t);
 	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)

 in split_asm_tac end;
 
 
 in
 
+val const_of_split_thm = const_of_split_thm;
+
 fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
 
 fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
 
 val mk_case_split_asm_tac = mk_case_split_asm_tac;