# HG changeset patch
# User wenzelm
# Date 1163069930 -3600
# Node ID 14d4e7f78e463012aa62a56a8a2cc62c27dfbedb
# Parent  de65ce2bfb32bf14d26f17159297068ddeb37a0f
removed obsolete locale_results;

diff -r de65ce2bfb32 -r 14d4e7f78e46 src/Pure/Isar/locale.ML
--- 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 **)