# HG changeset patch
# User wenzelm
# Date 1146859185 -7200
# Node ID fdb3642feb499a98500342100f4498b354863359
# Parent  179ad0076f75102c87fdc46a1b5f86e25923bad5
added syntax for _type_constraint_;

diff -r 179ad0076f75 -r fdb3642feb49 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri May 05 21:59:44 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Fri May 05 21:59:45 2006 +0200
@@ -371,6 +371,13 @@
   | type_tr' _ _ _ = raise Match;
 
 
+(* type constraints *)
+
+fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
+      Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
+  | type_constraint_tr' _ _ _ = raise Match;
+
+
 (* dependent / nondependent quantifiers *)
 
 fun variant_abs' (x, T, B) =
@@ -444,7 +451,8 @@
    ("_index", index_ast_tr')]);
 
 val pure_trfunsT =
-  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
+  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr'),
+   ("_type_constraint_", type_constraint_tr')];
 
 fun struct_trfuns structs =
   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
diff -r 179ad0076f75 -r fdb3642feb49 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri May 05 21:59:44 2006 +0200
+++ b/src/Pure/pure_thy.ML	Fri May 05 21:59:45 2006 +0200
@@ -569,6 +569,7 @@
     ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
     ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
     ("_idtypdummy", "type => idt",        Mixfix ("'_()\\<Colon>_", [], 0)),
+    ("_type_constraint_", "'a",           NoSyn),
     ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
     ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
diff -r 179ad0076f75 -r fdb3642feb49 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri May 05 21:59:44 2006 +0200
+++ b/src/Pure/type_infer.ML	Fri May 05 21:59:45 2006 +0200
@@ -173,7 +173,8 @@
           (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
       | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
       | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
-      | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
+      | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) =
+          constrain (pre_of (ps, t)) T
       | pre_of (ps, Bound i) = (ps, PBound i)
       | pre_of (ps, Abs (x, T, t)) =
           let
@@ -431,7 +432,7 @@
 
 fun constrain t T =
   if T = dummyT then t
-  else Const ("_type_constraint_", T) $ t;
+  else Const ("_type_constraint_", T --> T) $ t;
 
 
 (* user parameters *)