src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

       |> maps (fn (prems', frees') =>
         rewrite concl frees'
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
   in
-    map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
+    map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
   end
 
 end;