# HG changeset patch
# User wenzelm
# Date 954418842 -7200
# Node ID 49166d54942636f38c913ca6fea4d05b5eb96b74
# Parent  f0f7600b26058be7f0882f26e7b19c6564117a43
support polymorphic Vars;

diff -r f0f7600b2605 -r 49166d549426 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Mar 30 14:20:13 2000 +0200
+++ b/src/Pure/type_infer.ML	Thu Mar 30 14:20:42 2000 +0200
@@ -9,6 +9,7 @@
 sig
   val anyT: sort -> typ
   val logicT: typ
+  val polymorphicT: typ -> typ
   val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
     -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
     -> string list -> bool -> (indexname -> bool) -> term list -> typ list
@@ -99,6 +100,9 @@
 fun anyT S = TFree ("'_dummy_", S);
 val logicT = anyT logicS;
 
+(*indicate polymorphic Vars*)
+fun polymorphicT T = Type ("_polymorphic_", [T]);
+
 fun pretyp_of is_param (params, typ) =
   let
     fun add_parms (ps, TVar (xi as (x, _), S)) =
@@ -132,7 +136,8 @@
         (xi, mk_param []) :: ps
       else ps;
 
-    fun add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
+    fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps
+      | add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
       | add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1))
       | add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t)
       | add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u)
@@ -154,8 +159,10 @@
           (case const_type c of
             Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
           | None => raise TYPE ("No such constant: " ^ quote c, [], []))
+      | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) =
+          (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, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
       | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
       | pre_of (ps, Bound i) = (ps, PBound i)
       | pre_of (ps, Abs (x, T, t)) =
@@ -169,11 +176,8 @@
             val (ps'', u') = pre_of (ps', u);
           in (ps'', PAppl (t', u')) end;
 
-
     val (params', tm') = pre_of (params, tm);
-  in
-    ((vparams', params'), tm')
-  end;
+  in ((vparams', params'), tm') end;
 
 fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param);