equal
deleted
inserted
replaced
841 | _ => Conv.all_conv ctrm |
841 | _ => Conv.all_conv ctrm |
842 |
842 |
843 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
843 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
844 *} |
844 *} |
845 |
845 |
846 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
846 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
847 (* 1: does ? \<rightarrow> id *) |
847 (* 1: does ? \<rightarrow> id *) |
848 (* 2: does id \<rightarrow> ? *) |
848 (* 2: does ? \<rightarrow> non-id *) |
849 (* 3: does ? \<rightarrow> ? *) |
|
850 ML {* |
849 ML {* |
851 fun make_inst lhs t = |
850 fun make_inst lhs t = |
852 let |
851 let |
853 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
852 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
854 val _ $ (Abs (_, _, g)) = t; |
853 val _ $ (Abs (_, _, g)) = t; |