# HG changeset patch
# User wenzelm
# Date 1213821126 -7200
# Node ID a2db1e37977894d97f13956244ae4636053e3612
# Parent  49c81f6d7a0860d0a581994c5bc78f188d7bba8a
added type_constraint (formerly in type_infer.ML, which is now loaded later);

diff -r 49c81f6d7a08 -r a2db1e379778 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Jun 18 22:32:04 2008 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Jun 18 22:32:06 2008 +0200
@@ -11,6 +11,7 @@
   val sort_of_term: (sort -> sort) -> term -> sort
   val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
+  val type_constraint: typ -> term -> term
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
     (string -> bool * string) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> term -> term
@@ -105,16 +106,20 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
+fun type_constraint T t =
+  if T = dummyT then t
+  else Const ("_type_constraint_", T --> T) $ t;
+
 fun decode_term get_sort map_const map_free map_type map_sort tm =
   let
     val sort_env = term_sorts map_sort tm;
     val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
-          TypeInfer.constrain (decodeT typ) (decode t)
+          type_constraint (decodeT typ) (decode t)
       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
           if T = dummyT then Abs (x, decodeT typ, decode t)
-          else TypeInfer.constrain (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
+          else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
       | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =