equal
deleted
inserted
replaced
8 |
8 |
9 ML {* |
9 ML {* |
10 fun define_quotient_types binds tys alphas equivps ctxt = |
10 fun define_quotient_types binds tys alphas equivps ctxt = |
11 let |
11 let |
12 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
12 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
13 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), equivp) ctxt; |
13 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; |
14 val alpha_equivps = List.take (equivps, length alphas) |
14 val alpha_equivps = List.take (equivps, length alphas) |
15 val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
15 val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
16 val quot_thms = map fst thms; |
16 val quot_thms = map fst thms; |
17 val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; |
17 val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; |
18 val reps = map (hd o rev o snd o strip_comb) quots; |
18 val reps = map (hd o rev o snd o strip_comb) quots; |