# HG changeset patch
# User wenzelm
# Date 1301137300 -3600
# Node ID 74bf78db0d877dff215a14344e1fbaf3286551c3
# Parent  2ba15af46cb735a83ab6ed2ce447ea0ffb8a39d8
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
recovered printing of Hoare assign statements from 45d090186bbe;

diff -r 2ba15af46cb7 -r 74bf78db0d87 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 12:01:40 2011 +0100
@@ -93,20 +93,14 @@
           annquote_tr' (Syntax.const name) (r :: t :: ts)
       | annbexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
 
     fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | annassign_tr' _ = raise Match;
 
     fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
diff -r 2ba15af46cb7 -r 74bf78db0d87 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 12:01:40 2011 +0100
@@ -67,15 +67,9 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r 2ba15af46cb7 -r 74bf78db0d87 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 12:01:40 2011 +0100
@@ -237,15 +237,9 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r 2ba15af46cb7 -r 74bf78db0d87 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 26 12:01:40 2011 +0100
@@ -961,21 +961,11 @@
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
       (case dest_update ctxt c of
         SOME name =>
-          let
-            val opt_t =
-              (case k of
-                Abs (_, _, Abs (_, _, t) $ Bound 0) =>
-                  if null (loose_bnos t) then SOME t else NONE
-              | Abs (_, _, t) =>
-                  if null (loose_bnos t) then SOME t else NONE
-              | _ => NONE);
-          in
-            (case opt_t of
-              SOME t =>
-                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
-                  (field_updates_tr' ctxt u)
-            | NONE => ([], tm))
-          end
+          (case try Syntax.const_abs_tr' k of
+            SOME t =>
+              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
+                (field_updates_tr' ctxt u)
+          | NONE => ([], tm))
       | NONE => ([], tm))
   | field_updates_tr' _ tm = ([], tm);
 
diff -r 2ba15af46cb7 -r 74bf78db0d87 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 12:01:40 2011 +0100
@@ -10,6 +10,7 @@
   val eta_contract_raw: Config.raw
   val eta_contract: bool Config.T
   val atomic_abs_tr': string * typ * term -> term * term
+  val const_abs_tr': term -> term
   val mk_binder_tr: string * string -> string * (term list -> term)
   val mk_binder_tr': string * string -> string * (term list -> term)
   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
@@ -316,6 +317,13 @@
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
 
+fun const_abs_tr' t =
+  (case eta_abs t of
+    Abs (_, _, t') =>
+      if Term.is_dependent t' then raise Match
+      else incr_boundvars ~1 t'
+  | _ => raise Match);
+
 
 (* binders *)