--- a/src/HOL/Tools/Lifting/lifting_term.ML Wed May 02 18:26:10 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed May 02 19:02:16 2012 +0200
@@ -158,7 +158,8 @@
val thy = Proof_Context.theory_of ctxt'
val absT = rty --> qty
val schematic_absT = Logic.type_map (singleton (Variable.polymorphic ctxt')) absT
- val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,0)
+ 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
val subs = raw_match (schematic_rel_absT, absT) Vartab.empty
val rel_quot_thm_prems = (Logic.strip_imp_prems o prop_of) rel_quot_thm