# HG changeset patch
# User panny
# Date 1389203333 -3600
# Node ID 26166d7f6a15b8cdfe70d0035c94033cf118dc8b
# Parent  516adecd99dd5087b1698c046ad406d8c6cf07b9# Parent  9e632948ed568932a2532cee07da27f602c177aa
merge

diff -r 516adecd99dd -r 26166d7f6a15 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 08 17:26:42 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 08 18:48:53 2014 +0100
@@ -55,7 +55,7 @@
   transfer_rule - of the form T t f
   parametric_transfer_rule - of the form par_R t' t
   
-  Result: par_T t' f, after substituing op= for relations in par_T that relate
+  Result: par_T t' f, after substituing op= for relations in par_R that relate
     a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
     using Lifting_Term.merge_transfer_relations
 *)
diff -r 516adecd99dd -r 26166d7f6a15 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 08 17:26:42 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 08 18:48:53 2014 +0100
@@ -126,17 +126,6 @@
 
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
 
-fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
-  if provided_rty_name <> rty_of_qty_name then
-    raise QUOT_THM_INTERNAL (Pretty.block 
-        [Pretty.str ("The type " ^ quote provided_rty_name),
-         Pretty.brk 1,
-         Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
-         Pretty.brk 1,
-         Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")])
-  else
-    ()
-
 fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars =
   case try (get_rel_quot_thm ctxt) type_name of
     NONE => rty_Tvars ~~ qty_Tvars
@@ -176,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
@@ -192,14 +184,32 @@
           rel_quot_thm_prems
       end
 
-fun instantiate_rtys ctxt  (Type (rty_name, _)) (qty as Type (qty_name, _)) =
+fun instantiate_rtys ctxt rty (qty as Type (qty_name, _)) =
   let
     val quot_thm = get_quot_thm ctxt qty_name
-    val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
-    val _ = check_raw_types (rty_name, rs) qty_name
+    val ((rty_pat as Type (_, rty_pat_tys)), qty_pat) = quot_thm_rty_qty quot_thm
+    
+    fun inst_rty (Type (s, tys), Type (s', tys')) = 
+        if s = s' then Type (s', map inst_rty (tys ~~ tys'))
+        else raise QUOT_THM_INTERNAL (Pretty.block 
+          [Pretty.str "The type",
+           Pretty.brk 1,
+           Syntax.pretty_typ ctxt rty,
+           Pretty.brk 1,
+           Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
+           Pretty.brk 1,
+           Pretty.str "the correct raw type must be an instance of",
+           Pretty.brk 1,
+           Syntax.pretty_typ ctxt rty_pat])
+      | inst_rty (t as Type (_, _), TFree _) = t
+      | inst_rty ((TVar _), rty) = rty
+      | inst_rty ((TFree _), rty) = rty
+      | inst_rty (_, _) = error "check_raw_types: we should not be here"
+
+    val (Type (_, rtys')) = inst_rty (rty_pat, rty)
     val qtyenv = match ctxt equiv_match_err qty_pat qty
   in
-    map (Envir.subst_type qtyenv) rtys
+    (rtys', map (Envir.subst_type qtyenv) rty_pat_tys)
   end
   | instantiate_rtys _ _ _ = error "instantiate_rtys: not Type"
 
@@ -219,8 +229,8 @@
         end
       else
         let
-          val rtys' = instantiate_rtys ctxt rty qty
-          val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys')
+          val (rtys, rtys') = instantiate_rtys ctxt rty qty
+          val args = map (prove_schematic_quot_thm ctxt) (rtys ~~ rtys')
         in
           if forall is_id_quot args
           then
@@ -544,7 +554,7 @@
               else
                 all_args_conv parametrize_relation_conv ctm
             else
-              if forall op= (rargs ~~ (instantiate_rtys ctxt rty qty)) then
+              if forall op= (op~~ (instantiate_rtys ctxt rty qty)) then
                 let
                   val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq ctxt q)
                 in