author haftmann Wed, 26 May 2010 16:05:25 +0200 changeset 37135 636e6d8645d6 parent 37123 9cce71cd4bf0 child 37136 e0c9d3e49e15
normalized references to constant "split"
```--- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:05:25 2010 +0200
@@ -1,5 +1,4 @@
(*  Title:      HOL/Hoare/hoare_tac.ML
-    ID:         \$Id\$
Author:     Leonor Prensa Nieto & Tobias Nipkow

Derivation of the proof rules and, most importantly, the VCG tactic.
@@ -17,8 +16,8 @@
local open HOLogic in

(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const ("split",_) \$ (Abs(x,T,t))) = Free (x, T)::abs2list t
-  | abs2list (Abs(x,T,t)) = [Free (x, T)]
+fun abs2list (Const (@{const_name split}, _) \$ Abs (x, T, t)) = Free (x, T) :: abs2list t
+  | abs2list (Abs (x, T, t)) = [Free (x, T)]
| abs2list _ = [];

(** maps {(x1,...,xn). t} to [x1,...,xn] **)
@@ -33,7 +32,7 @@
else let val z  = mk_abstupleC w body;
val T2 = case z of Abs(_,T,_) => T
| Const (_, Type (_,[_, Type (_,[T,_])])) \$ _ => T;
-       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
+       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
\$ absfree (n, T, z) end end;

(** maps [x1,...,xn] to (x1,...,xn) and types**)```
```--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 26 16:05:25 2010 +0200
@@ -323,7 +323,7 @@
let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
-  | get_decls sign Clist ((Const("split",_)) \$ trm) = get_decls sign Clist trm
+  | get_decls sign Clist ((Const (@{const_name split}, _)) \$ trm) = get_decls sign Clist trm
| get_decls sign Clist trm = (Clist,trm);

fun make_mu_def sign ((tt \$ LHS) \$ (ttt \$ RHS)) =
@@ -389,9 +389,9 @@
val t2 = t1 \$ ParamDeclTerm
in t2 end;

-fun is_fundef (( Const("==",_) \$ _) \$ ((Const("split",_)) \$ _)) = true |
-is_fundef (( Const("==",_) \$ _) \$ Abs(x_T_t)) = true
-| is_fundef _ = false;
+fun is_fundef (Const("==", _) \$ _ \$ (Const (@{const_name split}, _) \$ _)) = true
+  | is_fundef (Const("==", _) \$ _ \$ Abs _) = true
+  | is_fundef _ = false;

fun make_mucke_fun_def sign ((_ \$ LHS) \$ RHS) =
let   (* fun dest_atom (Const t) = dest_Const (Const t)```
```--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 26 16:05:25 2010 +0200
@@ -2015,7 +2015,7 @@
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))

-fun strip_split_abs (Const ("split", _) \$ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name split}, _) \$ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
```
```--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed May 26 16:05:25 2010 +0200
@@ -179,7 +179,7 @@
|> maps (fn (res, (names, prems)) =>
flatten' (betapply (g, res)) (names, prems))
end)
-        | Const (@{const_name "split"}, _) =>
+        | Const (@{const_name split}, _) =>
(let
val (_, g :: res :: args) = strip_comb t
val [res1, res2] = Name.variant_list names ["res1", "res2"]```
```--- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 26 16:05:25 2010 +0200
@@ -560,12 +560,12 @@
end
end

-  | (((t1 as Const (@{const_name "split"}, _)) \$ Abs (v1, ty, Abs(v1', ty', s1))),
-     ((t2 as Const (@{const_name "split"}, _)) \$ Abs (v2, _ , Abs(v2', _  , s2)))) =>
+  | (((t1 as Const (@{const_name split}, _)) \$ Abs (v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name split}, _)) \$ Abs (v2, _ , Abs(v2', _  , s2)))) =>
regularize_trm ctxt (t1, t2) \$ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))

-  | (((t1 as Const (@{const_name "split"}, _)) \$ Abs (v1, ty, s1)),
-     ((t2 as Const (@{const_name "split"}, _)) \$ Abs (v2, _ , s2))) =>
+  | (((t1 as Const (@{const_name split}, _)) \$ Abs (v1, ty, s1)),
+     ((t2 as Const (@{const_name split}, _)) \$ Abs (v2, _ , s2))) =>
regularize_trm ctxt (t1, t2) \$ Abs (v1, ty, regularize_trm ctxt (s1, s2))

| (t1 \$ t2, t1' \$ t2') =>```
```--- a/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 16:05:25 2010 +0200
@@ -195,8 +195,8 @@
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);

local
-fun mk_uncurry(xt,yt,zt) =
-    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
+fun mk_uncurry (xt, yt, zt) =
+    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const("Pair",_) \$ M \$ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -276,7 +276,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";

-local  fun ucheck t = (if #Name(dest_const t) = "split" then t
+local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
else raise Match)
in
fun dest_pabs used tm =```