# HG changeset patch
# User kuncar
# Date 1389196797 -3600
# Node ID 1c000fa0fdf503bf6ead06e27b750103e3fd93ec
# Parent  dcd4dcf2639543ee0d3a8a806812452d7ff1363a
ensure that schematic type variables are fresh in rty

diff -r dcd4dcf26395 -r 1c000fa0fdf5 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 08 12:05:42 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 08 16:59:57 2014 +0100
@@ -165,10 +165,13 @@
         val qty = Type (type_name, qty_Tvars)
         val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm
         val schematic_rel_absT = quot_term_absT rel_quot_thm_concl;
-        val ctxt' = Variable.declare_typ schematic_rel_absT ctxt
-        val thy = Proof_Context.theory_of ctxt'
+        val thy = Proof_Context.theory_of ctxt
         val absT = rty --> qty
-        val schematic_absT = Logic.type_map (singleton (Variable.polymorphic ctxt')) absT
+        val schematic_absT = 
+          absT 
+          |> Logic.type_map (singleton (Variable.polymorphic ctxt))
+          |> Logic.incr_tvar (maxidx_of_typ schematic_rel_absT + 1) 
+            (* because absT can already contain schematic variables from rty patterns *)
         val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT]
         val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,maxidx)
           handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT