author | wenzelm |
Thu, 09 Nov 2006 11:58:50 +0100 | |
changeset 21264 | 14d4e7f78e46 |
parent 21263 | de65ce2bfb32 |
child 21265 | b8db43faaf9e |
--- 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 **)