# HG changeset patch
# User haftmann
# Date 1274882725 -7200
# Node ID 636e6d8645d6fac17ce24c544e1839a612c70394
# Parent  9cce71cd4bf0812e132a39581c91fa14120eccb4
normalized references to constant "split"

diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Hoare/hoare_tac.ML
--- 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**)
diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Modelcheck/mucke_oracle.ML
--- 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)
diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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
 
diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- 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"]
diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Tools/Quotient/quotient_term.ML
--- 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') =>
diff -r 9cce71cd4bf0 -r 636e6d8645d6 src/HOL/Tools/TFL/usyntax.ML
--- 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 =