diff -r 548e2d3105b9 -r 5fe899199f85 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Sat Jun 14 17:49:24 2008 +0200 +++ b/src/CCL/Hered.thy Sat Jun 14 23:19:51 2008 +0200 @@ -97,7 +97,8 @@ done ML {* - fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i + fun HTT_coinduct_tac ctxt s i = + RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i *} lemma HTT_coinduct3: @@ -109,7 +110,8 @@ ML {* val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3} -fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i +fun HTT_coinduct3_tac ctxt s i = + RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i val HTTgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})