diff -r fd3c60ad9155 -r cb1a1c94b4cd src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/Hered.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      CCL/Hered.thy
-    ID:         $Id$
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
@@ -113,7 +112,7 @@
   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
 
 val HTTgenIs =
-  map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
+  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   ["true : HTTgen(R)",
    "false : HTTgen(R)",
    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",