src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Sat Nov 19 15:34:37 2011 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Nov 19 16:16:33 2011 +0100
@@ -895,7 +895,7 @@
       |> fst;  (* FIXME duplication to add_thmss *)
   in
     ctxt
-    |> Locale.add_thmss target Thm.lemmaK facts
+    |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
     |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
       fn thy =>
         Locale.add_dependency target