tuned;

--- a/src/Pure/Syntax/syntax_phases.ML	Mon May 27 13:44:02 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 13:55:04 2013 +0200
@@ -515,6 +515,34 @@
 
 (* term_to_ast *)
 
+local
+
+fun mark_aprop tm =
+  let
+    fun aprop t = Syntax.const "_aprop" $ t;
+
+    fun is_prop Ts t =
+      fastype_of1 (Ts, t) = propT handle TERM _ => false;
+
+    fun is_term (Const ("Pure.term", _) $ _) = true
+      | is_term _ = false;
+
+    fun mark _ (t as Const _) = t
+      | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
+      | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
+      | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
+      | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
+      | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
+      | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
+          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
+          else mark Ts t1 $ mark Ts t2
+      | mark Ts (t as t1 $ t2) =
+          (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
+            (mark Ts t1 $ mark Ts t2);
+  in mark [] tm end;
+
+in
+
 fun term_to_ast idents is_syntax_const ctxt trf tm =
   let
     val show_types =
@@ -527,6 +555,25 @@
 
     val {structs, fixes} = idents;
 
+    fun prune_typs (t_seen as (Const _, _)) = t_seen
+      | prune_typs (t as Free (x, ty), seen) =
+          if ty = dummyT then (t, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
+          else (t, t :: seen)
+      | prune_typs (t as Var (xi, ty), seen) =
+          if ty = dummyT then (t, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
+          else (t, t :: seen)
+      | prune_typs (t_seen as (Bound _, _)) = t_seen
+      | prune_typs (Abs (x, ty, t), seen) =
+          let val (t', seen') = prune_typs (t, seen);
+          in (Abs (x, ty, t'), seen') end
+      | prune_typs (t1 $ t2, seen) =
+          let
+            val (t1', seen') = prune_typs (t1, seen);
+            val (t2', seen'') = prune_typs (t2, seen');
+          in (t1' $ t2', seen'') end;
+
     fun mark_atoms ((t as Const (c, _)) $ u) =
           if member (op =) Pure_Thy.token_markers c
           then t $ u else mark_atoms t $ mark_atoms u
@@ -548,25 +595,6 @@
           else Syntax.const "_var" $ t
       | mark_atoms a = a;
 
-    fun prune_typs (t_seen as (Const _, _)) = t_seen
-      | prune_typs (t as Free (x, ty), seen) =
-          if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
-          else (t, t :: seen)
-      | prune_typs (t as Var (xi, ty), seen) =
-          if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
-          else (t, t :: seen)
-      | prune_typs (t_seen as (Bound _, _)) = t_seen
-      | prune_typs (Abs (x, ty, t), seen) =
-          let val (t', seen') = prune_typs (t, seen);
-          in (Abs (x, ty, t'), seen') end
-      | prune_typs (t1 $ t2, seen) =
-          let
-            val (t1', seen') = prune_typs (t1, seen);
-            val (t2', seen'') = prune_typs (t2, seen');
-          in (t1' $ t2', seen'') end;
-
     fun ast_of tm =
       (case strip_comb tm of
         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
@@ -598,12 +626,14 @@
       else simple_ast_of ctxt t;
   in
     tm
-    |> Syntax_Trans.prop_tr'
+    |> mark_aprop
     |> show_types ? (#1 o prune_typs o rpair [])
     |> mark_atoms
     |> ast_of
   end;
 
+end;
+
 
 
 (** unparse **)

--- a/src/Pure/Syntax/syntax_trans.ML	Mon May 27 13:44:02 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon May 27 13:55:04 2013 +0200
@@ -39,7 +39,6 @@
   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
-  val prop_tr': term -> term
   val variant_abs: string * typ * term -> string * term
   val variant_abs': string * typ * term -> string * term
   val dependent_tr': string * string -> term list -> term
@@ -378,37 +377,6 @@
   | idtyp_ast_tr' _ _ = raise Match;
 
 
-(* meta propositions *)
-
-fun prop_tr' tm =
-  let
-    fun aprop t = Syntax.const "_aprop" $ t;
-
-    fun is_prop Ts t =
-      fastype_of1 (Ts, t) = propT handle TERM _ => false;
-
-    fun is_term (Const ("Pure.term", _) $ _) = true
-      | is_term _ = false;
-
-    fun tr' _ (t as Const _) = t
-      | tr' Ts (t as Const ("_bound", _) $ u) =
-          if is_prop Ts u then aprop t else t
-      | tr' _ (t as Free (x, T)) =
-          if T = propT then aprop (Syntax.free x) else t
-      | tr' _ (t as Var (xi, T)) =
-          if T = propT then aprop (Syntax.var xi) else t
-      | tr' Ts (t as Bound _) =
-          if is_prop Ts t then aprop t else t
-      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
-      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
-          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
-          else tr' Ts t1 $ tr' Ts t2
-      | tr' Ts (t as t1 $ t2) =
-          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
-            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
-  in tr' [] tm end;
-
-
 (* meta implication *)
 
 fun impl_ast_tr' asts =