author | wenzelm |
Fri, 02 Aug 2002 11:12:34 +0200 | |
changeset 13442 | 70479ec9f44f |
parent 13441 | d6d620639243 |
child 13443 | 1c3327c348b3 |
--- 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;