# HG changeset patch
# User wenzelm
# Date 1130531289 -7200
# Node ID 79417bfbdbd7c13544901f7a806f412fb638a1e0
# Parent  1095d2213b9ddc24b794b2357399247649646bcc
tuned ProofContext.export interfaces;

diff -r 1095d2213b9d -r 79417bfbdbd7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Oct 28 22:28:07 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Oct 28 22:28:09 2005 +0200
@@ -1814,7 +1814,7 @@
     val thy_ctxt = ProofContext.init thy;
     val loc = prep_locale thy raw_loc;
     val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
-    val export = ProofContext.export_standard_view stmt loc_ctxt thy_ctxt;
+    val export = ProofContext.export_view stmt loc_ctxt thy_ctxt;
 
     val (ctxt', (args', facts)) = activate_note prep_facts (loc_ctxt, args);
     val facts' =
@@ -2017,7 +2017,7 @@
         |> snd;
     val (ctxt, (_, facts)) = activate_facts (K I)
       (pred_ctxt, axiomify predicate_axioms elemss');
-    val export = ProofContext.export_standard_view predicate_statement ctxt pred_ctxt;
+    val export = ProofContext.export_view predicate_statement ctxt pred_ctxt;
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
     val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
   in
@@ -2084,7 +2084,7 @@
 
     fun after_qed' (goal_ctxt, raw_results) results =
       let val res = results |> (map o map)
-          (ProofContext.export_standard elems_ctxt' locale_ctxt) in
+          (ProofContext.export elems_ctxt' locale_ctxt) in
         curry (add_thmss kind locale ((names ~~ locale_attss) ~~ res)) locale_ctxt
         #-> (fn res' =>
           if name = "" andalso null locale_atts then I