equal
deleted
inserted
replaced
9 fun define_quotient_types binds tys alphas equivps ctxt = |
9 fun define_quotient_types binds tys alphas equivps ctxt = |
10 let |
10 let |
11 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
11 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
12 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; |
12 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; |
13 val alpha_equivps = List.take (equivps, length alphas) |
13 val alpha_equivps = List.take (equivps, length alphas) |
14 val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
14 val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
15 val quot_thms = map fst thms; |
15 val qtys = map #qtyp qinfo; |
16 val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; |
|
17 val reps = map (hd o rev o snd o strip_comb) quots; |
|
18 val qtys = map (domain_type o fastype_of) reps; |
|
19 in |
16 in |
20 (qtys, ctxt') |
17 (qtys, ctxt') |
21 end |
18 end |
22 *} |
19 *} |
23 |
20 |