src/HOLCF/adm_tac.ML
changeset 16842 5979c46853d1
parent 16062 f8110bd9957f
child 16935 4d7f19d340e8
     1.1 --- a/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -80,9 +80,9 @@
     1.4  
     1.5  
     1.6  (*figure out internal names*)
     1.7 -val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
     1.8 -val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
     1.9 -val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
    1.10 +val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
    1.11 +val cont_name = Sign.intern_const (the_context ()) "cont";
    1.12 +val adm_name = Sign.intern_const (the_context ()) "adm";
    1.13  
    1.14  
    1.15  (*** check whether type of terms in list is chain finite ***)