1.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 01 18:22:46 2002 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Aug 02 11:12:34 2002 +0200
     1.3 @@ -937,7 +937,7 @@
     1.4          in
     1.5            def_thy |> have_thmss_qualified "" bname
     1.6              [((introN, [ContextRules.intro_query_global None]), [([intro], [])]),
     1.7 -             ((axiomsN, []), [(map Drule.standard axioms, [])])]
     1.8 +             ((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])]
     1.9            |> #1 |> rpair ([cstatement], axioms)
    1.10          end;
    1.11    in (thy'', (elemss', view)) end;