# HG changeset patch
# User wenzelm
# Date 1028279554 -7200
# Node ID 70479ec9f44f83e96aa16bb207f6723b99fb9f1f
# Parent  d6d6206392435591d62b67cca208dab7d049ae9c
declare projected "axioms" as "elim?";

diff -r d6d620639243 -r 70479ec9f44f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 01 18:22:46 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 02 11:12:34 2002 +0200
@@ -937,7 +937,7 @@
         in
           def_thy |> have_thmss_qualified "" bname
             [((introN, [ContextRules.intro_query_global None]), [([intro], [])]),
-             ((axiomsN, []), [(map Drule.standard axioms, [])])]
+             ((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])]
           |> #1 |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', view)) end;