src/HOL/Tools/Quotient/quotient_term.ML
changeset 38694 9db37e912ee4
parent 38624 9bb0016f7e60
child 38718 c7cbbb18eabe
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 24 15:08:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 24 22:38:45 2010 +0800
     1.3 @@ -225,12 +225,16 @@
     1.4               val qtyenv = match ctxt absrep_match_err qty_pat qty
     1.5               val args_aux = map (double_lookup rtyenv qtyenv) vs
     1.6               val args = map (absrep_fun flag ctxt) args_aux
     1.7 -             val map_fun = mk_mapfun ctxt vs rty_pat
     1.8 -             val result = list_comb (map_fun, args)
     1.9             in
    1.10               if forall is_identity args
    1.11               then absrep_const flag ctxt s'
    1.12 -             else mk_fun_compose flag (absrep_const flag ctxt s', result)
    1.13 +             else 
    1.14 +               let
    1.15 +                 val map_fun = mk_mapfun ctxt vs rty_pat
    1.16 +                 val result = list_comb (map_fun, args)
    1.17 +               in
    1.18 +                 mk_fun_compose flag (absrep_const flag ctxt s', result)
    1.19 +               end
    1.20             end
    1.21      | (TFree x, TFree x') =>
    1.22          if x = x'
    1.23 @@ -332,14 +336,18 @@
    1.24             val qtyenv = match ctxt equiv_match_err qty_pat qty
    1.25             val args_aux = map (double_lookup rtyenv qtyenv) vs
    1.26             val args = map (equiv_relation ctxt) args_aux
    1.27 -           val rel_map = mk_relmap ctxt vs rty_pat
    1.28 -           val result = list_comb (rel_map, args)
    1.29             val eqv_rel = get_equiv_rel ctxt s'
    1.30             val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
    1.31           in
    1.32             if forall is_eq args
    1.33             then eqv_rel'
    1.34 -           else mk_rel_compose (result, eqv_rel')
    1.35 +           else 
    1.36 +             let 
    1.37 +               val rel_map = mk_relmap ctxt vs rty_pat
    1.38 +               val result = list_comb (rel_map, args)
    1.39 +             in
    1.40 +               mk_rel_compose (result, eqv_rel')
    1.41 +             end
    1.42           end
    1.43        | _ => HOLogic.eq_const rty
    1.44  
    1.45 @@ -740,10 +748,14 @@
    1.46       false: raw -> quotient
    1.47  *)
    1.48  fun mk_ty_subst qtys direction ctxt =
    1.49 +let
    1.50 +  val thy = ProofContext.theory_of ctxt  
    1.51 +in
    1.52    Quotient_Info.quotdata_dest ctxt
    1.53     |> map (fn x => (#rtyp x, #qtyp x))
    1.54 -   |> filter (fn (_, qty) => member (op =) qtys qty)
    1.55 +   |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
    1.56     |> map (if direction then swap else I)
    1.57 +end
    1.58  
    1.59  fun mk_trm_subst qtys direction ctxt =
    1.60  let