equal
deleted
inserted
replaced
7 |
7 |
8 ML {* |
8 ML {* |
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)), 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 (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
15 val quot_thms = map fst thms; |
15 val quot_thms = map fst thms; |
16 val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; |
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; |
17 val reps = map (hd o rev o snd o strip_comb) quots; |