# HG changeset patch
# User wenzelm
# Date 1304017564 -7200
# Node ID 13b41fb77649d0f4814ef1fd4935ecdb325cdff3
# Parent  2b8c34f53388888c2b6843b2f6f666c797bea4b0
literal facts `prop` may contain dummy patterns;

diff -r 2b8c34f53388 -r 13b41fb77649 NEWS
--- a/NEWS	Thu Apr 28 20:20:49 2011 +0200
+++ b/NEWS	Thu Apr 28 21:06:04 2011 +0200
@@ -44,6 +44,10 @@
 
   declare [[unique_names = false]]
 
+* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
+that the result needs to be unique, which means fact specifications
+may have to be refined after enriching a proof context.
+
 
 *** HOL ***
 
diff -r 2b8c34f53388 -r 13b41fb77649 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 28 20:20:49 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 28 21:06:04 2011 +0200
@@ -841,16 +841,20 @@
 fun retrieve_thms pick ctxt (Facts.Fact s) =
       let
         val (_, pos) = Syntax.read_token s;
-        val prop = Syntax.read_prop (set_mode mode_default ctxt) s
+        val prop =
+          Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);
+        fun err msg = error (msg ^ Position.str_of pos ^ ":\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 [th])));
+          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
+        val results = map_filter (try prove_fact) (potential_facts ctxt prop');
         val res =
-          (case get_first (try prove_fact) (potential_facts ctxt prop) of
-            SOME res => res
-          | NONE => error ("Failed to retrieve literal fact" ^ Position.str_of pos ^ ":\n" ^
-              Syntax.string_of_term ctxt prop))
+          (case distinct Thm.eq_thm_prop results of
+            [res] => res
+          | [] => err "Failed to retrieve literal fact"
+          | _ => err "Ambiguous specification of literal fact");
       in pick "" [res] end
   | retrieve_thms pick ctxt xthmref =
       let