--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200
@@ -273,7 +273,7 @@
val var = Free (var_name, fpT);
val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var);
- val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
+ val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
in
Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN