# HG changeset patch
# User ballarin
# Date 1227632853 -3600
# Node ID 9d19554bc2a08e24391fb3bc2c2a0612e6d57b99
# Parent  6f28fa3bc430b276bfe2c72ae750277ac328204b
Use standard export function.

diff -r 6f28fa3bc430 -r 9d19554bc2a0 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Nov 25 18:07:01 2008 +0100
+++ b/src/Pure/Isar/element.ML	Tue Nov 25 18:07:33 2008 +0100
@@ -536,9 +536,6 @@
 
 local
 
-fun axioms_export axs _ As =
-  (satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
-
 fun activate_elem (Fixes fixes) ctxt =
       ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
   | activate_elem (Constrains _) ctxt =
@@ -549,7 +546,7 @@
         val ts = maps (map #1 o #2) asms';
         val (_, ctxt') =
           ctxt |> fold Variable.auto_fixes ts
-          |> ProofContext.add_assms_i (axioms_export []) asms';
+          |> ProofContext.add_assms_i Assumption.presume_export asms';
       in ([], ctxt') end
   | activate_elem (Defines defs) ctxt =
       let