# HG changeset patch
# User nipkow
# Date 1040550129 -3600
# Node ID 9dd78dab72bc754e04346d1f52b310d489fd928d
# Parent  52d1b293da7f8bce7c52f0c63aa5c0b8edf2288c
*** empty log message ***

diff -r 52d1b293da7f -r 9dd78dab72bc src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Fri Dec 20 10:54:33 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy	Sun Dec 22 10:42:09 2002 +0100
@@ -39,7 +39,7 @@
 translations
   "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
   "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
-  "p^.f"       ==  "f(addr p)"
+  "p^.f"       =>  "f(addr p)"
 
 
 text "An example due to Suzuki:"
diff -r 52d1b293da7f -r 9dd78dab72bc src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Dec 20 10:54:33 2002 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Dec 22 10:42:09 2002 +0100
@@ -9,6 +9,7 @@
 signature SYN_TRANS0 =
 sig
   val eta_contract: bool ref
+  val atomic_abs_tr': string * typ * term -> term * term
   val mk_binder_tr: string * string -> string * (term list -> term)
   val mk_binder_tr': string * string -> string * (term list -> term)
   val dependent_tr': string * string -> term list -> term
@@ -225,6 +226,10 @@
     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
 
 
+fun atomic_abs_tr' (x,T,t) = 
+  let val [xT] = rename_wrt_term t [(x,T)];
+  in  (mark_boundT xT, subst_bound (mark_bound(fst xT), t)) end;
+
 fun abs_ast_tr' (*"_abs"*) asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)