# HG changeset patch
# User wenzelm
# Date 886674035 -3600
# Node ID 53b2463ca84c435239a7ea9f43c680167dc3fa06
# Parent  0e034d76932ef3f8facc41c1f67954b85401cd87
added param;

diff -r 0e034d76932e -r 53b2463ca84c src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Feb 05 11:19:51 1998 +0100
+++ b/src/Pure/type.ML	Thu Feb 05 11:20:35 1998 +0100
@@ -64,6 +64,7 @@
   val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
     -> (indexname * sort) list -> indexname -> sort
   val constrain: term -> typ -> term
+  val param: string list -> string * sort -> typ
   val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
     -> type_sig -> (string -> typ option) -> (indexname -> typ option)
     -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
@@ -817,6 +818,12 @@
   else Const ("_type_constraint_", T) $ t;
 
 
+(* user parameters *)
+
+fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
+fun param used (x, S) = TVar (("?" ^ variant used x, 0), S);
+
+
 (* decode_types *)
 
 (*transform parse tree into raw term*)
@@ -866,12 +873,6 @@
   freeze: if true then generated parameters are turned into TFrees, else TVars
 *)
 
-(*user-supplied inference parameters: ??x.i *)
-fun q_is_param (x, _) =
-  (case explode x of
-    "?" :: _ => true
-  | _ => false);
-
 fun infer_types prt prT tsig const_type def_type def_sort
     map_const map_type map_sort used freeze pat_Ts raw_ts =
   let
@@ -882,7 +883,7 @@
       map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
     val (ts, Ts, unifier) =
       TypeInfer.infer_types prt prT const_type classrel arities used freeze
-        q_is_param raw_ts' pat_Ts';
+        is_param raw_ts' pat_Ts';
   in
     (ts, unifier)
   end;