# HG changeset patch
# User wenzelm
# Date 1247566201 -7200
# Node ID 1a35de4112bb27dc09754424c15f1c8a36a31b6a
# Parent  fafefd0b341cd4d884538a96adf79f18e1adb24e
tuned paramify_vars: Term_Subst.map_atypsT_option;

diff -r fafefd0b341c -r 1a35de4112bb src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Jul 14 10:56:43 2009 +0200
+++ b/src/Pure/type_infer.ML	Tue Jul 14 12:10:01 2009 +0200
@@ -39,7 +39,8 @@
 fun is_param (x, _: int) = String.isPrefix "?" x;
 fun param i (x, S) = TVar (("?" ^ x, i), S);
 
-val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
+val paramify_vars =
+  perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
 
 val paramify_dummies =
   let