1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:20:09 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:21:41 2012 +0100
     1.3 @@ -72,9 +72,6 @@
     1.4  
     1.5  fun defined_mapfun_data ctxt s =
     1.6    Symtab.defined (Enriched_Type.entries ctxt) s
     1.7 -  
     1.8 -(* makes a Free out of a TVar *)
     1.9 -fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    1.10  
    1.11  (* looks up the (varified) rty and qty for
    1.12     a quotient definition
    1.13 @@ -279,35 +276,10 @@
    1.14      SOME map_data => Const (#relmap map_data, dummyT)
    1.15    | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    1.16  
    1.17 -(* takes two type-environments and looks
    1.18 -   up in both of them the variable v, which
    1.19 -   must be listed in the environment
    1.20 -*)
    1.21 -fun double_lookup rtyenv qtyenv v =
    1.22 -  let
    1.23 -    val v' = fst (dest_TVar v)
    1.24 -  in
    1.25 -    (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
    1.26 -  end
    1.27 -
    1.28 -fun mk_relmap ctxt vs rty =
    1.29 -  let
    1.30 -    val vs' = map (mk_Free) vs
    1.31 -
    1.32 -    fun mk_relmap_aux rty =
    1.33 -      case rty of
    1.34 -        TVar _ => mk_Free rty
    1.35 -      | Type (_, []) => HOLogic.eq_const rty
    1.36 -      | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
    1.37 -      | _ => raise LIFT_MATCH ("mk_relmap (default)")
    1.38 -  in
    1.39 -    fold_rev Term.lambda vs' (mk_relmap_aux rty)
    1.40 -  end
    1.41 -
    1.42  fun get_equiv_rel thy s =
    1.43    (case Quotient_Info.lookup_quotients thy s of
    1.44      SOME qdata => #equiv_rel qdata
    1.45 -  | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
    1.46 +  | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
    1.47  
    1.48  fun equiv_match_err ctxt ty_pat ty =
    1.49    let
    1.50 @@ -336,11 +308,10 @@
    1.51            end
    1.52          else
    1.53            let
    1.54 -            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
    1.55 -            val rtyenv = match ctxt equiv_match_err rty_pat rty
    1.56 +            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
    1.57              val qtyenv = match ctxt equiv_match_err qty_pat qty
    1.58 -            val args_aux = map (double_lookup rtyenv qtyenv) vs
    1.59 -            val args = map (equiv_relation ctxt) args_aux
    1.60 +            val rtys' = map (Envir.subst_type qtyenv) rtys
    1.61 +            val args = map (equiv_relation ctxt) (tys ~~ rtys')
    1.62              val eqv_rel = get_equiv_rel ctxt s'
    1.63              val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
    1.64            in
    1.65 @@ -348,8 +319,7 @@
    1.66              then eqv_rel'
    1.67              else
    1.68                let
    1.69 -                val rel_map = mk_relmap ctxt vs rty_pat
    1.70 -                val result = list_comb (rel_map, args)
    1.71 +                val result = list_comb (get_relmap ctxt s, args)
    1.72                in
    1.73                  mk_rel_compose (result, eqv_rel')
    1.74                end