src/HOL/Tools/res_axioms.ML
changeset 24137 8d7896398147
parent 24042 968f42fe6836
child 24215 5458fbf18276
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Aug 02 23:18:13 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Aug 03 16:28:15 2007 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    inside that theory -- because it's needed for Skolemization *)
     1.5  
     1.6  (*This will refer to the final version of theory ATP_Linkup.*)
     1.7 -val recon_thy_ref = Theory.self_ref (the_context ());
     1.8 +val recon_thy_ref = Theory.check_thy @{theory}
     1.9  
    1.10  (*If called while ATP_Linkup is being created, it will transfer to the
    1.11    current version. If called afterward, it will transfer to the final version.*)