diff -r d3ee6315ca22 -r 15fcad6eb956 src/Pure/Syntax/syntax_trans.ML
--- 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 =