equal
deleted
inserted
replaced
82 for example for: (?'a list * ?'b) |
82 for example for: (?'a list * ?'b) |
83 it produces: %a b. prod_map (map a) b |
83 it produces: %a b. prod_map (map a) b |
84 *) |
84 *) |
85 fun mk_mapfun ctxt vs rty = |
85 fun mk_mapfun ctxt vs rty = |
86 let |
86 let |
87 val vs' = map (mk_Free) vs |
87 val vs' = map mk_Free vs |
88 |
88 |
89 fun mk_mapfun_aux rty = |
89 fun mk_mapfun_aux rty = |
90 case rty of |
90 case rty of |
91 TVar _ => mk_Free rty |
91 TVar _ => mk_Free rty |
92 | Type (_, []) => mk_identity rty |
92 | Type (_, []) => mk_identity rty |
101 *) |
101 *) |
102 fun get_rty_qty ctxt s = |
102 fun get_rty_qty ctxt s = |
103 let |
103 let |
104 val thy = ProofContext.theory_of ctxt |
104 val thy = ProofContext.theory_of ctxt |
105 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
105 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
106 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
106 val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn |
107 in |
107 in |
108 (#rtyp qdata, #qtyp qdata) |
108 (#rtyp qdata, #qtyp qdata) |
109 end |
109 end |
110 |
110 |
111 (* takes two type-environments and looks |
111 (* takes two type-environments and looks |