src/HOL/Hoare/hoare_syntax.ML
changeset 55414 eab03e9cee8a
parent 51693 1eb533ea1480
child 55659 4089f6e98ab9
     1.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
     1.6    | mk_abstuple (x :: xs) body =
     1.7 -      Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
     1.8 +      Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
     1.9  
    1.10  fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
    1.11    | mk_fbody x e (y :: xs) =
    1.12 @@ -82,21 +82,21 @@
    1.13  local
    1.14  
    1.15  fun dest_abstuple
    1.16 -      (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
    1.17 +      (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
    1.18          subst_bound (Syntax.free v, dest_abstuple body)
    1.19    | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
    1.20    | dest_abstuple tm = tm;
    1.21  
    1.22 -fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    1.23 +fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    1.24    | abs2list (Abs (x, T, t)) = [Free (x, T)]
    1.25    | abs2list _ = [];
    1.26  
    1.27 -fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
    1.28 +fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
    1.29    | mk_ts (Abs (x, _, t)) = mk_ts t
    1.30    | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
    1.31    | mk_ts t = [t];
    1.32  
    1.33 -fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
    1.34 +fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
    1.35        (Syntax.free x :: abs2list t, mk_ts t)
    1.36    | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
    1.37    | mk_vts t = raise Match;
    1.38 @@ -106,7 +106,7 @@
    1.39        if t = Bound i then find_ch vts (i - 1) xs
    1.40        else (true, (v, subst_bounds (xs, t)));
    1.41  
    1.42 -fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
    1.43 +fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
    1.44    | is_f (Abs (x, _, t)) = true
    1.45    | is_f t = false;
    1.46