1.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 11:59:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 16:05:25 2010 +0200
     1.3 @@ -195,8 +195,8 @@
     1.4  fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
     1.5  
     1.6  local
     1.7 -fun mk_uncurry(xt,yt,zt) =
     1.8 -    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
     1.9 +fun mk_uncurry (xt, yt, zt) =
    1.10 +    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    1.11  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
    1.12    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
    1.13  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
    1.14 @@ -276,7 +276,7 @@
    1.15    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
    1.16  
    1.17  
    1.18 -local  fun ucheck t = (if #Name(dest_const t) = "split" then t
    1.19 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
    1.20                         else raise Match)
    1.21  in
    1.22  fun dest_pabs used tm =