1.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Oct 16 22:44:36 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Oct 16 22:44:37 2008 +0200
     1.3 @@ -125,16 +125,23 @@
     1.4    in (syn, binder_tr) end;
     1.5  
     1.6  
     1.7 +(* type propositions *)
     1.8 +
     1.9 +fun mk_type ty = Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty);
    1.10 +
    1.11 +fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
    1.12 +  | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
    1.13 +
    1.14 +fun sort_constraint_tr (*"_sort_constraint"*) [ty] =
    1.15 +      Lexicon.const "Pure.sort_constraint" $ mk_type ty
    1.16 +  | sort_constraint_tr (*"_sort_constraint"*) ts = raise TERM ("sort_constraint_tr", ts);
    1.17 +
    1.18 +
    1.19  (* meta propositions *)
    1.20  
    1.21  fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
    1.22    | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
    1.23  
    1.24 -fun ofclass_tr (*"_ofclass"*) [ty, cls] =
    1.25 -      cls $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
    1.26 -        (Lexicon.const "itself" $ ty))
    1.27 -  | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
    1.28 -
    1.29  
    1.30  (* meta implication *)
    1.31  
    1.32 @@ -155,8 +162,7 @@
    1.33  
    1.34  (* type/term reflection *)
    1.35  
    1.36 -fun type_tr (*"_TYPE"*) [ty] =
    1.37 -      Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
    1.38 +fun type_tr (*"_TYPE"*) [ty] = mk_type ty
    1.39    | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
    1.40  
    1.41  fun term_tr [t] = Lexicon.const "Pure.term" $ t
    1.42 @@ -327,11 +333,20 @@
    1.43  
    1.44  fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] =
    1.45        if c = "_constrain" then
    1.46 -        Ast.Appl [ Ast.Constant a,  Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
    1.47 +        Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
    1.48        else raise Match
    1.49    | idtyp_ast_tr' _ _ = raise Match;
    1.50  
    1.51  
    1.52 +(* type propositions *)
    1.53 +
    1.54 +fun type_prop_tr' _ (*"_type_prop"*) T [Const ("Pure.sort_constraint", _)] =
    1.55 +      Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
    1.56 +  | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
    1.57 +      Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
    1.58 +  | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
    1.59 +
    1.60 +
    1.61  (* meta propositions *)
    1.62  
    1.63  fun prop_tr' tm =
    1.64 @@ -355,17 +370,13 @@
    1.65            if is_prop Ts t then aprop t else t
    1.66        | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
    1.67        | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    1.68 -          if is_prop Ts t andalso not (is_term t) then Const ("_mk_ofclass", T) $ tr' Ts t1
    1.69 +          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
    1.70            else tr' Ts t1 $ tr' Ts t2
    1.71        | tr' Ts (t as t1 $ t2) =
    1.72            (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
    1.73              then I else aprop) (tr' Ts t1 $ tr' Ts t2);
    1.74    in tr' [] tm end;
    1.75  
    1.76 -fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =
    1.77 -      Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
    1.78 -  | mk_ofclass_tr' _ (*"_mk_ofclass"*) T ts = raise TYPE ("mk_ofclass_tr'", [T], ts);
    1.79 -
    1.80  
    1.81  (* meta implication *)
    1.82  
    1.83 @@ -462,16 +473,16 @@
    1.84     ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
    1.85     ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
    1.86    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    1.87 -   ("\\<^fixed>meta_conjunction", conjunction_tr), ("_TYPE", type_tr),
    1.88 -   ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr), ("_index", index_tr)],
    1.89 +   ("_sort_constraint", sort_constraint_tr), ("\\<^fixed>meta_conjunction", conjunction_tr),
    1.90 +   ("_TYPE", type_tr), ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr),
    1.91 +   ("_index", index_tr)],
    1.92    ([]: (string * (term list -> term)) list),
    1.93    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    1.94     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
    1.95     ("_index", index_ast_tr')]);
    1.96  
    1.97  val pure_trfunsT =
    1.98 -  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr'),
    1.99 -   ("_type_constraint_", type_constraint_tr')];
   1.100 +  [("_type_prop", type_prop_tr'), ("TYPE", type_tr'), ("_type_constraint_", type_constraint_tr')];
   1.101  
   1.102  fun struct_trfuns structs =
   1.103    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);