src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -391,7 +391,7 @@
         |> 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;