--- a/src/HOL/Hoare/Hoare_Logic.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Mon Jun 28 15:03:07 2010 +0200
@@ -68,7 +68,7 @@
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 Syntax.free b
| mk_fbody a e ((b,_)::xs) =
@@ -128,21 +128,21 @@
(*** 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;
@@ -152,7 +152,7 @@
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;
*}