38 fun ty_lift_error1 lthy rty qty = |
38 fun ty_lift_error1 lthy rty qty = |
39 let |
39 let |
40 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
40 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
41 val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."] |
41 val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."] |
42 in |
42 in |
43 raise LIFT_MATCH (space_implode " " msg) |
43 error (space_implode " " msg) |
44 end |
44 end |
45 |
45 |
46 fun ty_lift_error2 lthy rty qty = |
46 fun ty_lift_error2 lthy rty qty = |
47 let |
47 let |
48 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
48 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
49 val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."] |
49 val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."] |
50 in |
50 in |
51 raise LIFT_MATCH (space_implode " " msg) |
51 error (space_implode " " msg) |
52 end |
52 end |
53 |
53 |
54 fun get_fun_aux lthy s fs = |
54 fun get_fun_aux lthy s fs = |
55 case (maps_lookup (ProofContext.theory_of lthy) s) of |
55 case (maps_lookup (ProofContext.theory_of lthy) s) of |
56 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
56 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
57 | NONE => raise LIFT_MATCH (space_implode " " ["No map function for type", quote s, "."]) |
57 | NONE => error (space_implode " " ["No map function for type", quote s, "."]) |
58 |
58 |
59 fun get_const flag lthy _ qty = |
59 fun get_const flag lthy _ qty = |
60 (* FIXME: check here that _ and qty are related *) |
60 (* FIXME: check here that _ and qty are related *) |
61 let |
61 let |
62 val thy = ProofContext.theory_of lthy |
62 val thy = ProofContext.theory_of lthy |