1317 (Type (@{type_name fun}, old_Ts)) t1] |
1317 (Type (@{type_name fun}, old_Ts)) t1] |
1318 | Const _ $ t1 $ t2 => |
1318 | Const _ $ t1 $ t2 => |
1319 construct_value ctxt |
1319 construct_value ctxt |
1320 (if new_s = @{type_name prod} then @{const_name Pair} |
1320 (if new_s = @{type_name prod} then @{const_name Pair} |
1321 else @{const_name PairBox}, new_Ts ---> new_T) |
1321 else @{const_name PairBox}, new_Ts ---> new_T) |
1322 (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] |
1322 (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] |
1323 [t1, t2]) |
1323 [t1, t2]) |
1324 | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) |
1324 | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) |
1325 else |
1325 else |
1326 raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) |
1326 raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) |
1327 | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) |
1327 | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) |