# HG changeset patch
# User wenzelm
# Date 878726617 -3600
# Node ID e0e5a2820ac108c696b4587e63a80dbacd248f3f
# Parent  e57d03a5fc73821d9266431f340dc194f26aa570
adapted pure_trfunsT;
added type_tr/tr';
eliminated mk_ofclassS_tr';

diff -r e57d03a5fc73 -r e0e5a2820ac1 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 05 11:42:19 1997 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Nov 05 11:43:37 1997 +0100
@@ -25,14 +25,14 @@
       (string * (term list -> term)) list *
       (string * (term list -> term)) list *
       (string * (Ast.ast list -> Ast.ast)) list
-  val pure_trfunsT: (string * (typ -> term list -> term)) list
+  val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
 end;
 
 signature SYN_TRANS =
 sig
   include SYN_TRANS1
   val abs_tr': term -> term
-  val prop_tr': bool -> term -> term
+  val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
@@ -117,6 +117,12 @@
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise AST ("bigimpl_ast_tr", asts);
 
 
+(* type reflection *)
+
+fun type_tr (*"_TYPE"*) [ty] =
+      const constrainC $ const "TYPE" $ (const "itself" $ ty)
+  | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
+
 
 (** print (ast) translations **)
 
@@ -215,10 +221,9 @@
 
 (* meta propositions *)
 
-fun prop_tr' show_sorts tm =
+fun prop_tr' tm =
   let
     fun aprop t = const "_aprop" $ t;
-    val mk_ofclass = if show_sorts then "_mk_ofclassS" else "_mk_ofclass";
 
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
@@ -232,7 +237,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 then Const ("_mk_ofclass", T) $ tr' Ts t1
           else tr' Ts t1 $ tr' Ts t2
       | tr' Ts (t as t1 $ t2) =
           (if is_Const (head_of t) orelse not (is_prop Ts t)
@@ -241,14 +246,9 @@
     tr' [] tm
   end;
 
-
-fun mk_ofclass_tr' (*"_mk_ofclass"*) T [t] =
-      const "_ofclass" $ term_of_typ false T $ t
-  | mk_ofclass_tr' (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
-
-fun mk_ofclassS_tr' (*"_mk_ofclassS"*) T [t] =
-      const "_ofclass" $ term_of_typ true T $ t
-  | mk_ofclassS_tr' (*"_mk_ofclassS"*) T ts = raise TYPE ("mk_ofclassS_tr'", [T], ts);
+fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =
+      const "_ofclass" $ term_of_typ show_sorts T $ t
+  | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
 
 
 (* meta implication *)
@@ -260,6 +260,13 @@
   | _ => raise Match);
 
 
+(* type reflection *)
+
+fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
+      list_comb (const "_TYPE" $ term_of_typ show_sorts T, ts)
+  | type_tr' _ _ _ = raise Match;
+
+
 (* dependent / nondependent quantifiers *)
 
 fun variant_abs' (x, T, B) =
@@ -283,13 +290,13 @@
    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
    ("_bigimpl", bigimpl_ast_tr)],
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
-   ("_K", k_tr)],
+   ("_TYPE", type_tr), ("_K", k_tr)],
   []: (string * (term list -> term)) list,
   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
 
 val pure_trfunsT =
-  [("_mk_ofclass", mk_ofclass_tr'), ("_mk_ofclassS", mk_ofclassS_tr')];
+  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];