changeset 28262 | aa7ca36d67fd |
parent 27239 | f2f42f9fa09d |
child 32010 | cb1a1c94b4cd |
--- a/src/CCL/Hered.thy Wed Sep 17 21:27:03 2008 +0200 +++ b/src/CCL/Hered.thy Wed Sep 17 21:27:08 2008 +0200 @@ -113,7 +113,7 @@ 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}) + map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono}) ["true : HTTgen(R)", "false : HTTgen(R)", "[| a : R; b : R |] ==> <a,b> : HTTgen(R)",