--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 22 16:15:50 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 22 16:39:34 2011 +0100
@@ -91,8 +91,10 @@
*}
(* com_tr *)
ML{*
-fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+fun com_tr (t as (Const (@{syntax_const "_assign"},_) $ x $ e)) xs =
+ (case Syntax.strip_positions x of
+ Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+ | _ => t)
| com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
| com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
@@ -103,15 +105,16 @@
| com_tr t _ = t (* if t is just a Free/Var *)
*}
-(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
+(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
ML{*
local
fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
| var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
- | vars_tr t = [var_tr t]
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
+ var_tr (Syntax.strip_positions idt) :: vars_tr vars
+ | vars_tr t = [var_tr (Syntax.strip_positions t)]
in
fun hoare_vars_tr [vars, pre, prg, post] =