export: added explicit term operation;

--- a/src/Pure/Isar/locale.ML	Wed Dec 06 21:19:02 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Dec 06 21:19:03 2006 +0100
@@ -873,9 +873,8 @@
 
 local
 
-fun axioms_export axs _ hyps =
-  Element.satisfy_thm axs
-  #> Drule.implies_intr_list (Library.drop (length axs, hyps));
+fun axioms_export axs _ As =
+  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
 
 
 (* NB: derived ids contain only facts at this stage *)

--- a/src/Pure/Isar/obtain.ML	Wed Dec 06 21:19:02 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Dec 06 21:19:03 2006 +0100
@@ -64,16 +64,21 @@
   --------
      B
 *)
-fun obtain_export fix_ctxt rule xs _ As thm =
+fun eliminate_term ctxt xs tm =
+  let
+    val vs = map (dest_Free o Thm.term_of) xs;
+    val bads = Term.fold_aterms (fn t as Free v =>
+      if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
+    val _ = null bads orelse
+      error ("Result contains obtained parameters: " ^
+        space_implode " " (map (ProofContext.string_of_term ctxt) bads));
+  in tm end;
+
+fun eliminate fix_ctxt rule xs As thm =
   let
     val thy = ProofContext.theory_of fix_ctxt;
 
-    val vs = map (dest_Free o Thm.term_of) xs;
-    val bads = Term.fold_aterms (fn t as Free v =>
-      if member (op =) vs v then insert (op aconv) t else I | _ => I) (Thm.prop_of thm) [];
-    val _ = null bads orelse
-      error ("Result contains obtained parameters: " ^
-        space_implode " " (map (ProofContext.string_of_term fix_ctxt) bads));
+    val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
     val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 
@@ -88,6 +93,9 @@
     |> singleton (Variable.export ctxt' fix_ctxt)
   end;
 
+fun obtain_export ctxt rule xs _ As =
+  (eliminate ctxt rule xs As, eliminate_term ctxt xs);
+
 
 
 (** obtain **)