# HG changeset patch
# User wenzelm
# Date 1150055968 -7200
# Node ID a525275d36dfe70559818f5ac2aa5777a85f5cd3
# Parent  28724aab4745a9de5498cf48918815f04fc0c4a8
improved treatment of TERM TYPE syntax;

diff -r 28724aab4745 -r a525275d36df src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sun Jun 11 21:59:27 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Jun 11 21:59:28 2006 +0200
@@ -327,6 +327,9 @@
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
+    fun is_term (Const ("ProtoPure.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
@@ -338,7 +341,7 @@
           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 then Const ("_mk_ofclass", T) $ tr' Ts t1
+          if is_prop Ts t andalso not (is_term t) then Const ("_mk_ofclass", 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)