normalized references to constant "split"
authorhaftmann
Wed May 26 16:05:25 2010 +0200 (2010-05-26)
changeset 37135636e6d8645d6
parent 37123 9cce71cd4bf0
child 37136 e0c9d3e49e15
normalized references to constant "split"
src/HOL/Hoare/hoare_tac.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/TFL/usyntax.ML
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 11:59:06 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:05:25 2010 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Hoare/hoare_tac.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
     1.7  
     1.8  Derivation of the proof rules and, most importantly, the VCG tactic.
     1.9 @@ -17,8 +16,8 @@
    1.10  local open HOLogic in
    1.11  
    1.12  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
    1.13 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    1.14 -  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    1.15 +fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    1.16 +  | abs2list (Abs (x, T, t)) = [Free (x, T)]
    1.17    | abs2list _ = [];
    1.18  
    1.19  (** maps {(x1,...,xn). t} to [x1,...,xn] **)
    1.20 @@ -33,7 +32,7 @@
    1.21          else let val z  = mk_abstupleC w body;
    1.22                   val T2 = case z of Abs(_,T,_) => T
    1.23                          | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    1.24 -       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    1.25 +       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    1.26            $ absfree (n, T, z) end end;
    1.27  
    1.28  (** maps [x1,...,xn] to (x1,...,xn) and types**)
     2.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 26 11:59:06 2010 +0200
     2.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 26 16:05:25 2010 +0200
     2.3 @@ -323,7 +323,7 @@
     2.4      let val VarAbs = Syntax.variant_abs(s,tp,trm);
     2.5      in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
     2.6      end
     2.7 -  | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
     2.8 +  | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
     2.9    | get_decls sign Clist trm = (Clist,trm);
    2.10  
    2.11  fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
    2.12 @@ -389,9 +389,9 @@
    2.13        val t2 = t1 $ ParamDeclTerm
    2.14    in t2 end;
    2.15  
    2.16 -fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
    2.17 -is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true 
    2.18 -| is_fundef _ = false; 
    2.19 +fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
    2.20 +  | is_fundef (Const("==", _) $ _ $ Abs _) = true 
    2.21 +  | is_fundef _ = false; 
    2.22  
    2.23  fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
    2.24    let   (* fun dest_atom (Const t) = dest_Const (Const t)
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 26 11:59:06 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 26 16:05:25 2010 +0200
     3.3 @@ -2015,7 +2015,7 @@
     3.4    | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
     3.5    | split_lambda t _ = raise (TERM ("split_lambda", [t]))
     3.6  
     3.7 -fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t
     3.8 +fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
     3.9    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
    3.10    | strip_split_abs t = t
    3.11  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed May 26 11:59:06 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed May 26 16:05:25 2010 +0200
     4.3 @@ -179,7 +179,7 @@
     4.4                |> maps (fn (res, (names, prems)) =>
     4.5                  flatten' (betapply (g, res)) (names, prems))
     4.6              end)
     4.7 -        | Const (@{const_name "split"}, _) => 
     4.8 +        | Const (@{const_name split}, _) => 
     4.9              (let
    4.10                val (_, g :: res :: args) = strip_comb t
    4.11                val [res1, res2] = Name.variant_list names ["res1", "res2"]
     5.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 26 11:59:06 2010 +0200
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 26 16:05:25 2010 +0200
     5.3 @@ -560,12 +560,12 @@
     5.4             end
     5.5         end
     5.6  
     5.7 -  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
     5.8 -     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
     5.9 +  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    5.10 +     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    5.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
    5.12  
    5.13 -  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
    5.14 -     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
    5.15 +  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
    5.16 +     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
    5.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
    5.18  
    5.19    | (t1 $ t2, t1' $ t2') =>
     6.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 11:59:06 2010 +0200
     6.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 16:05:25 2010 +0200
     6.3 @@ -195,8 +195,8 @@
     6.4  fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
     6.5  
     6.6  local
     6.7 -fun mk_uncurry(xt,yt,zt) =
     6.8 -    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
     6.9 +fun mk_uncurry (xt, yt, zt) =
    6.10 +    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    6.11  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
    6.12    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
    6.13  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
    6.14 @@ -276,7 +276,7 @@
    6.15    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
    6.16  
    6.17  
    6.18 -local  fun ucheck t = (if #Name(dest_const t) = "split" then t
    6.19 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
    6.20                         else raise Match)
    6.21  in
    6.22  fun dest_pabs used tm =