src/HOLCF/Tools/Domain/domain_isomorphism.ML

         in (n, thmL) :: mk_unfold_thms ns thmR end;
     val unfold_binds = map (Binding.suffix_name "_unfold") binds;
 
     (* register unfold theorems *)
     val (unfold_thms, thy) =
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   in
     ((proj_thms, unfold_thms), thy)
   end;
 

       |>> ListPair.unzip;
 
     (* prove isomorphism and isodefl rules *)
     fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
       let
-        fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
+        fun make thm = Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]);
         val rep_iso_thm = make @{thm domain_rep_iso};
         val abs_iso_thm = make @{thm domain_abs_iso};
         val isodefl_thm = make @{thm isodefl_abs_rep};
         val rep_iso_bind = Binding.name "rep_iso";
         val abs_iso_bind = Binding.name "abs_iso";

       | conjuncts (n::ns) thm = let
           val thmL = thm RS @{thm conjunct1};
           val thmR = thm RS @{thm conjunct2};
         in (n, thmL):: conjuncts ns thmR end;
     val (isodefl_thms, thy) = thy |>
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
         (conjuncts isodefl_binds isodefl_thm);
     val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
 
     (* prove map_ID theorems *)
     fun prove_map_ID_thm