1.1 --- a/NEWS	Thu Apr 28 20:20:49 2011 +0200
     1.2 +++ b/NEWS	Thu Apr 28 21:06:04 2011 +0200
     1.3 @@ -44,6 +44,10 @@
     1.4  
     1.5    declare [[unique_names = false]]
     1.6  
     1.7 +* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
     1.8 +that the result needs to be unique, which means fact specifications
     1.9 +may have to be refined after enriching a proof context.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  

     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 28 20:20:49 2011 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 28 21:06:04 2011 +0200
     2.3 @@ -841,16 +841,20 @@
     2.4  fun retrieve_thms pick ctxt (Facts.Fact s) =
     2.5        let
     2.6          val (_, pos) = Syntax.read_token s;
     2.7 -        val prop = Syntax.read_prop (set_mode mode_default ctxt) s
     2.8 +        val prop =
     2.9 +          Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
    2.10            |> singleton (Variable.polymorphic ctxt);
    2.11 +        fun err msg = error (msg ^ Position.str_of pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
    2.12  
    2.13 +        val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
    2.14          fun prove_fact th =
    2.15 -          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])));
    2.16 +          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
    2.17 +        val results = map_filter (try prove_fact) (potential_facts ctxt prop');
    2.18          val res =
    2.19 -          (case get_first (try prove_fact) (potential_facts ctxt prop) of
    2.20 -            SOME res => res
    2.21 -          | NONE => error ("Failed to retrieve literal fact" ^ Position.str_of pos ^ ":\n" ^
    2.22 -              Syntax.string_of_term ctxt prop))
    2.23 +          (case distinct Thm.eq_thm_prop results of
    2.24 +            [res] => res
    2.25 +          | [] => err "Failed to retrieve literal fact"
    2.26 +          | _ => err "Ambiguous specification of literal fact");
    2.27        in pick "" [res] end
    2.28    | retrieve_thms pick ctxt xthmref =
    2.29        let