src/HOL/Hoare/Hoare_Logic_Abort.thy

   in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
 in
 
 fun mk_abstuple [x] body = abs (x, body)
   | mk_abstuple (x::xs) body =
-      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
 
 fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
   | mk_fbody a e ((b,_)::xs) =
       Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
 

 
 (*****************************************************************************)
 
 (*** print translations ***)
 ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
       subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple trm = trm;
 
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   | abs2list (Abs(x,T,t)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
   | mk_ts (Abs(x,_,t)) = mk_ts t
   | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   | mk_ts t = [t];
 
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
            ((Syntax.free x)::(abs2list t), mk_ts t)
   | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   | mk_vts t = raise Match;
 
 fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
   | find_ch ((v,t)::vts) i xs =
       if t = Bound i then find_ch vts (i-1) xs
       else (true, (v, subst_bounds (xs,t)));
 
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
 *}
 
 (* assn_tr' & bexp_tr'*)