src/Provers/splitter.ML

 infix 4 addsplits delsplits;
 
 signature SPLITTER_DATA =
 sig
   structure Simplifier: SIMPLIFIER
-  val mk_meta_eq    : thm -> thm
+  val mk_eq         : thm -> thm
   val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
   val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
   val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
   val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
   val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)

 val Const ("==>", _) $ (Const ("Trueprop", _) $
          (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
 
 fun split_format_err() = error("Wrong format for split rule");
 
-fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
+fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
      Const("==", _)$(Var _$t)$c =>
         (case strip_comb t of
            (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
          | _              => split_format_err())
    | _ => split_format_err();

    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
 fun split_tac [] i = no_tac
   | split_tac splits i =
-  let val splits = map Data.mk_meta_eq splits;
+  let val splits = map Data.mk_eq splits;
       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))
                 | _ => split_format_err())