tuned paramify_vars: Term_Subst.map_atypsT_option;
authorwenzelm
Tue Jul 14 12:10:01 2009 +0200 (2009-07-14)
changeset 320021a35de4112bb
parent 32001 fafefd0b341c
child 32003 befec6450fd6
tuned paramify_vars: Term_Subst.map_atypsT_option;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Tue Jul 14 10:56:43 2009 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Jul 14 12:10:01 2009 +0200
     1.3 @@ -39,7 +39,8 @@
     1.4  fun is_param (x, _: int) = String.isPrefix "?" x;
     1.5  fun param i (x, S) = TVar (("?" ^ x, i), S);
     1.6  
     1.7 -val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
     1.8 +val paramify_vars =
     1.9 +  perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
    1.10  
    1.11  val paramify_dummies =
    1.12    let