src/CCL/Hered.thy

--- 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)",