# HG changeset patch
# User wenzelm
# Date 1128718758 -7200
# Node ID 32bb237158a5fee717467dfffcfc9bafffe3cf08
# Parent  274eaa114c6db6a934fce25f79a23a7d549c53bd
print_translation: does not handle _idtdummy;

diff -r 274eaa114c6d -r 32bb237158a5 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Fri Oct 07 22:59:17 2005 +0200
+++ b/src/CCL/Term.thy	Fri Oct 07 22:59:18 2005 +0200
@@ -56,6 +56,7 @@
 ML {*
 (** Quantifier translations: variable binding **)
 
+(* FIXME does not handle "_idtdummy" *)
 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
 
 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
diff -r 274eaa114c6d -r 32bb237158a5 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Oct 07 22:59:17 2005 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Fri Oct 07 22:59:18 2005 +0200
@@ -101,7 +101,7 @@
   | com_tr t _ = t (* if t is just a Free/Var *)
 *}
 
-(* triple_tr *)
+(* triple_tr *)    (* FIXME does not handle "_idtdummy" *)
 ML{*
 local
 
diff -r 274eaa114c6d -r 32bb237158a5 src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Fri Oct 07 22:59:17 2005 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy	Fri Oct 07 22:59:18 2005 +0200
@@ -103,7 +103,7 @@
   | com_tr t _ = t (* if t is just a Free/Var *)
 *}
 
-(* triple_tr *)
+(* triple_tr *)  (* FIXME does not handle "_idtdummy" *)
 ML{*
 local
 
diff -r 274eaa114c6d -r 32bb237158a5 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Fri Oct 07 22:59:17 2005 +0200
+++ b/src/HOL/Hoare/Separation.thy	Fri Oct 07 22:59:18 2005 +0200
@@ -55,6 +55,7 @@
  "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
  "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
 
+(* FIXME does not handle "_idtdummy" *)
 ML{*
 (* free_tr takes care of free vars in the scope of sep. logic connectives:
    they are implicitly applied to the heap *)
diff -r 274eaa114c6d -r 32bb237158a5 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:17 2005 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:18 2005 +0200
@@ -35,7 +35,7 @@
 
 translations
   "PI x:A. B" => "Pi A (%x. B)"
-  "A -> B" => "Pi A (_K B)"
+  "A -> B" => "Pi A (%_. B)"
   "%x:A. f" == "restrict (%x. f) A"
 
 constdefs