| changeset 21686 | 4f5f6c685ab4 |
| parent 21665 | ba07e24dc941 |
| child 21701 | 627c90b310c1 |
--- 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 *)