# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 37e1431cc213dcc3d55d92071d8bde9c15c5c39d
# Parent  3f740034b927c1908241066c1cd1de447f45b315
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

diff -r 3f740034b927 -r 37e1431cc213 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -201,12 +201,11 @@
 fun is_type_surely_infinite ctxt infinite_Ts T =
   tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
 
-fun monomorphic_term subst t =
+fun monomorphic_term subst =
   map_types (map_type_tvar (fn v =>
       case Type.lookup subst v of
         SOME typ => typ
-      | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
-                            \variable", [t]))) t
+      | NONE => TVar v))
 
 fun eta_expand _ t 0 = t
   | eta_expand Ts (Abs (s, T, t')) n =