# HG changeset patch
# User wenzelm
# Date 1300808374 -3600
# Node ID 8cd4783904d8083ef61682d66780068097530672
# Parent  006095137a81eafca0c2ebe34ad43bf6afe99fc0
Hoare syntax: strip positions where they crash translation functions;
re-unified some clones (!);

diff -r 006095137a81 -r 8cd4783904d8 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 22 16:15:50 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 22 16:39:34 2011 +0100
@@ -89,8 +89,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
@@ -105,11 +107,12 @@
 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 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] =
diff -r 006095137a81 -r 8cd4783904d8 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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] =