--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:20:09 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:21:41 2012 +0100
@@ -72,9 +72,6 @@
fun defined_mapfun_data ctxt s =
Symtab.defined (Enriched_Type.entries ctxt) s
-
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
(* looks up the (varified) rty and qty for
a quotient definition
@@ -279,35 +276,10 @@
SOME map_data => Const (#relmap map_data, dummyT)
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-(* takes two type-environments and looks
- up in both of them the variable v, which
- must be listed in the environment
-*)
-fun double_lookup rtyenv qtyenv v =
- let
- val v' = fst (dest_TVar v)
- in
- (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
- end
-
-fun mk_relmap ctxt vs rty =
- let
- val vs' = map (mk_Free) vs
-
- fun mk_relmap_aux rty =
- case rty of
- TVar _ => mk_Free rty
- | Type (_, []) => HOLogic.eq_const rty
- | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
- | _ => raise LIFT_MATCH ("mk_relmap (default)")
- in
- fold_rev Term.lambda vs' (mk_relmap_aux rty)
- end
-
fun get_equiv_rel thy s =
(case Quotient_Info.lookup_quotients thy s of
SOME qdata => #equiv_rel qdata
- | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
+ | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
fun equiv_match_err ctxt ty_pat ty =
let
@@ -336,11 +308,10 @@
end
else
let
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = match ctxt equiv_match_err rty_pat rty
+ val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
val qtyenv = match ctxt equiv_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (equiv_relation ctxt) args_aux
+ val rtys' = map (Envir.subst_type qtyenv) rtys
+ val args = map (equiv_relation ctxt) (tys ~~ rtys')
val eqv_rel = get_equiv_rel ctxt s'
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
in
@@ -348,8 +319,7 @@
then eqv_rel'
else
let
- val rel_map = mk_relmap ctxt vs rty_pat
- val result = list_comb (rel_map, args)
+ val result = list_comb (get_relmap ctxt s, args)
in
mk_rel_compose (result, eqv_rel')
end