# HG changeset patch
# User wenzelm
# Date 1469191352 -7200
# Node ID e7b9ae541718ff00194849f6577d9ccc4024b18c
# Parent  e308f15cc8a7205a381e781f7295263a1ab0ff37
tuned;

diff -r e308f15cc8a7 -r e7b9ae541718 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jul 22 11:01:10 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 22 14:42:32 2016 +0200
@@ -1006,7 +1006,7 @@
           | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
 
         val markup =
-          (Markup.entity Markup.literal_factN "")
+          Markup.entity Markup.literal_factN ""
           |> Markup.properties (Position.def_properties_of thm_pos);
         val _ = Context_Position.report_generic context pos markup;
       in pick true ("", thm_pos) [thm] end