src/Pure/Isar/proof_context.ML
changeset 27867 6e6a159671d4
parent 27828 edafacb690a3
child 28017 4919bd124a58
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 14 16:52:51 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 14 16:52:52 2008 +0200
     1.3 @@ -863,14 +863,16 @@
     1.4  
     1.5  (* fact_tac *)
     1.6  
     1.7 -fun comp_incr_tac [] _ st = no_tac st
     1.8 -  | comp_incr_tac (th :: ths) i st =
     1.9 -      (Goal.compose_hhf_tac (Drule.incr_indexes st th) i APPEND comp_incr_tac ths i) st;
    1.10 +fun comp_incr_tac [] _ = no_tac
    1.11 +  | comp_incr_tac (th :: ths) i =
    1.12 +      (fn st => Goal.compose_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
    1.13  
    1.14  fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
    1.15  
    1.16 -fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) =>
    1.17 -  fact_tac (Facts.could_unify (facts_of ctxt) (Term.strip_all_body goal)) i);
    1.18 +fun potential_facts ctxt prop =
    1.19 +  Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
    1.20 +
    1.21 +fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
    1.22  
    1.23  
    1.24  (* get_thm(s) *)
    1.25 @@ -879,11 +881,19 @@
    1.26  
    1.27  fun retrieve_thms pick ctxt (Facts.Fact s) =
    1.28        let
    1.29 +        val (_, pos) = Syntax.read_token s;
    1.30          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
    1.31            |> singleton (Variable.polymorphic ctxt);
    1.32 -        val th = Goal.prove ctxt [] [] prop (K (ALLGOALS (some_fact_tac ctxt)))
    1.33 -          handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
    1.34 -      in pick "" [th] end
    1.35 +
    1.36 +        fun prove_fact th =
    1.37 +          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])))
    1.38 +          |> Thm.default_position_of th;
    1.39 +        val res =
    1.40 +          (case get_first (try prove_fact) (potential_facts ctxt prop) of
    1.41 +            SOME res => res
    1.42 +          | NONE => error ("Failed to retrieve literal fact" ^ Position.str_of pos ^ ":\n" ^
    1.43 +              Syntax.string_of_term ctxt prop))
    1.44 +      in pick "" [res] end
    1.45    | retrieve_thms pick ctxt xthmref =
    1.46        let
    1.47          val thy = theory_of ctxt;
    1.48 @@ -937,7 +947,7 @@
    1.49      val name = full_name ctxt bname;
    1.50      val facts = PureThy.name_thmss false name (map (apfst (get ctxt)) raw_facts);
    1.51      fun app (th, attrs) x =
    1.52 -      swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ [PureThy.kind k])) (x, th));
    1.53 +      swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ [Thm.kind k])) (x, th));
    1.54      val (res, ctxt') = fold_map app facts ctxt;
    1.55      val thms = PureThy.name_thms false false name (flat res);
    1.56      val Mode {stmt, ...} = get_mode ctxt;