| changeset 21264 | 14d4e7f78e46 |
| parent 21234 | fb84ab52f23b |
| child 21361 | 653d1631f997 |
--- a/src/Pure/Isar/locale.ML Thu Nov 09 11:58:49 2006 +0100 +++ b/src/Pure/Isar/locale.ML Thu Nov 09 11:58:50 2006 +0100 @@ -1547,8 +1547,6 @@ #> note_thmss_registrations kind loc args'); in (facts, ctxt'') end; -fun locale_results kind loc args = add_thmss kind loc (map (apsnd Thm.simple_fact) args); - (** define locales **)