1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 28 20:20:49 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 28 21:06:04 2011 +0200
     1.3 @@ -841,16 +841,20 @@
     1.4  fun retrieve_thms pick ctxt (Facts.Fact s) =
     1.5        let
     1.6          val (_, pos) = Syntax.read_token s;
     1.7 -        val prop = Syntax.read_prop (set_mode mode_default ctxt) s
     1.8 +        val prop =
     1.9 +          Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
    1.10            |> singleton (Variable.polymorphic ctxt);
    1.11 +        fun err msg = error (msg ^ Position.str_of pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
    1.12  
    1.13 +        val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
    1.14          fun prove_fact th =
    1.15 -          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])));
    1.16 +          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
    1.17 +        val results = map_filter (try prove_fact) (potential_facts ctxt prop');
    1.18          val res =
    1.19 -          (case get_first (try prove_fact) (potential_facts ctxt prop) of
    1.20 -            SOME res => res
    1.21 -          | NONE => error ("Failed to retrieve literal fact" ^ Position.str_of pos ^ ":\n" ^
    1.22 -              Syntax.string_of_term ctxt prop))
    1.23 +          (case distinct Thm.eq_thm_prop results of
    1.24 +            [res] => res
    1.25 +          | [] => err "Failed to retrieve literal fact"
    1.26 +          | _ => err "Ambiguous specification of literal fact");
    1.27        in pick "" [res] end
    1.28    | retrieve_thms pick ctxt xthmref =
    1.29        let