# HG changeset patch
# User wenzelm
# Date 1137444915 -3600
# Node ID a95c2adc89006657c0c3d6811dd7b91137179563
# Parent  86b3f73e3fd552f174a833f07804a6528aa1761b
put_facts: do not pretend local thms were named;

diff -r 86b3f73e3fd5 -r a95c2adc8900 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jan 16 21:55:14 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Jan 16 21:55:15 2006 +0100
@@ -1461,13 +1461,10 @@
 (* add facts to locale in theory *)
 
 fun put_facts loc args thy =
-  let
-    val {predicate, import, elems, params, regs} = the_locale thy loc;
-    val note = Notes (map (fn ((a, atts), bs) =>
-      ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args);
+  let val {predicate, import, elems, params, regs} = the_locale thy loc
   in
     thy |> put_locale loc {predicate = predicate, import = import,
-      elems = elems @ [(note, stamp ())], params = params, regs = regs}
+      elems = elems @ [(Notes args, stamp ())], params = params, regs = regs}
   end;
 
 (* add theorem to locale and theory,