--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Jul 26 17:24:54 2015 +0200
@@ -43,13 +43,9 @@
let
val num_frees = length frees;
val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
- fun find s = find_index (curry (op =) s) frees;
- fun mk_cfp (f as ((s, _), T)) =
- (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s)));
- val cfps = map mk_cfp fs;
- in
- Drule.cterm_instantiate cfps thm
- end;
+ fun find x = find_index (curry (op =) x) frees;
+ fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x)));
+ in infer_instantiate ctxt (map mk_inst fs) thm end;
val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;