1049       | Bound j => if i = j then error "make_inst" else t

  1049       | Bound j => if i = j then error "make_inst" else t

  1050       | _ => t);

  1050       | _ => t);

  1051   in (f, Abs ("x", T, mk_abs 0 g)) end;

  1051   in (f, Abs ("x", T, mk_abs 0 g)) end;

  1052 *}

  1052 *}

  1053 

  1053 

  1056   case (term_of ctrm) of

  1058   case (term_of ctrm) of

  1057     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>

  1059     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>

  1058     let

  1060     let

  1059       val (ty_b, ty_a) = dest_fun_type (fastype_of r1);

  1061       val (ty_b, ty_a) = dest_fun_type (fastype_of r1);

  1060       val (ty_c, ty_d) = dest_fun_type (fastype_of a2);

  1062       val (ty_c, ty_d) = dest_fun_type (fastype_of a2);

  1072     end

  1074     end

  1073   | _ => Conv.all_conv ctrm

  1075   | _ => Conv.all_conv ctrm

  1074 *}

  1076 *}

  1075 

  1077 

  1076 ML {*

  1078 ML {*

  1081 *}

  1083 *}

  1082 

  1084 

  1083 (*

  1085 (*

  1084  Cleaning the theorem consists of 6 kinds of rewrites.

  1086  Cleaning the theorem consists of 6 kinds of rewrites.

  1085  The first two need to be done before fun_map is unfolded

  1087  The first two need to be done before fun_map is unfolded