--- 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**)