position information for literal facts;
Markup.entry may have empty kind/name;

--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Tue Jun 21 14:42:47 2016 +0200
@@ -16,7 +16,7 @@
     val names = map Thm.get_name_hint thms
     val add_info = if null names then I else suffix (":\n" ^ commas names)
 
-    val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
+    val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre)))
 
     fun metis ctxt =
       Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Jun 21 14:42:47 2016 +0200
@@ -468,6 +468,7 @@
     val named_locals = Facts.dest_static true [global_facts] local_facts
     val unnamed_locals =
       Facts.props local_facts
+      |> map #1
       |> filter (is_useful_unnamed_local_fact ctxt)
       |> map (pair "" o single)
 

--- a/src/Pure/Isar/proof_context.ML	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jun 21 14:42:47 2016 +0200
@@ -945,15 +945,18 @@
 
 in
 
-fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
-
 fun potential_facts ctxt prop =
   let
     val body = Term.strip_all_body prop;
-    val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts;
+    val vacuous =
+      filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts
+      |> map (rpair Position.none);
   in Facts.could_unify (facts_of ctxt) body @ vacuous end;
 
-fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
+fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
+
+fun some_fact_tac ctxt =
+  SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i);
 
 end;
 
@@ -993,18 +996,23 @@
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);
-        fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
+        fun err ps msg =
+          error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop);
 
         val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
-        fun prove_fact th =
-          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
-        val results = map_filter (try prove_fact) (potential_facts ctxt prop');
-        val thm =
-          (case distinct Thm.eq_thm_prop results of
-            [thm] => thm
-          | [] => err "Failed to retrieve literal fact"
-          | _ => err "Ambiguous specification of literal fact");
-      in pick true ("", Position.none) [thm] end
+        fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
+        val results = map_filter (try (apfst prove)) (potential_facts ctxt prop');
+        val (thm, thm_pos) =
+          (case distinct (eq_fst Thm.eq_thm_prop) results of
+            [res] => res
+          | [] => err [] "Failed to retrieve literal fact"
+          | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
+
+        val markup =
+          (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
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
@@ -1450,7 +1458,7 @@
 fun pretty_local_facts verbose ctxt =
   let
     val facts = facts_of ctxt;
-    val props = Facts.props facts;
+    val props = map #1 (Facts.props facts);
     val local_facts =
       (if null props then [] else [("<unnamed>", props)]) @
       Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;

--- a/src/Pure/PIDE/markup.ML	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Jun 21 14:42:47 2016 +0200
@@ -86,6 +86,7 @@
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
+  val literal_factN: string val literal_fact: string -> T
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
@@ -343,7 +344,9 @@
 val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
-fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
+fun entity kind name =
+  (entityN,
+    (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 fun get_entity_kind (name, props) =
   if name = entityN then AList.lookup (op =) props kindN
@@ -441,6 +444,7 @@
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
+val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
 val method_modifierN = "method_modifier";
 

--- a/src/Pure/PIDE/markup.scala	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Jun 21 14:42:47 2016 +0200
@@ -95,10 +95,9 @@
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
-          (props, props) match {
-            case (Kind(kind), Name(name)) => Some((kind, name))
-            case _ => None
-          }
+          val kind = Kind.unapply(props).getOrElse("")
+          val name = Name.unapply(props).getOrElse("")
+          Some((kind, name))
         case _ => None
       }
   }

--- a/src/Pure/facts.ML	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/facts.ML	Tue Jun 21 14:42:47 2016 +0200
@@ -36,8 +36,8 @@
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
   val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
-  val props: T -> thm list
-  val could_unify: T -> term -> thm list
+  val props: T -> (thm * Position.T) list
+  val could_unify: T -> term -> (thm * Position.T) list
   val merge: T * T -> T
   val add_static: Context.generic -> {strict: bool, index: bool} ->
     binding * thm list -> T -> string * T
@@ -134,7 +134,7 @@
 
 datatype T = Facts of
  {facts: fact Name_Space.table,
-  props: thm Net.net};
+  props: (thm * Position.T) Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
 
@@ -227,7 +227,7 @@
 
 (* indexed props *)
 
-val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
+val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
 
 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
 fun could_unify (Facts {props, ...}) = Net.unify_term props;
@@ -250,11 +250,13 @@
 fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   let
     val ths' = map Thm.trim_context ths;
+    val pos = #2 (Position.default (Binding.pos_of b));
+
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
       else Name_Space.define context strict (b, Static ths') facts;
     val props' = props
-      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths';
+      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
   in (name, make_facts facts' props') end;
 
 

--- a/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 14:42:47 2016 +0200
@@ -604,6 +604,7 @@
             val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 =
               if (name == "") kind1
+              else if (kind1 == "") quote(name)
               else kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =