--- a/src/Pure/Isar/proof.ML Fri Jun 05 13:26:12 2015 +0200
+++ b/src/Pure/Isar/proof.ML Fri Jun 05 13:41:06 2015 +0200
@@ -67,6 +67,8 @@
val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val with_thmss: ((thm list * attribute list) list) list -> state -> state
val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
+ val supply: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+ val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
val using: ((thm list * attribute list) list) list -> state -> state
val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val unfolding: ((thm list * attribute list) list) list -> state -> state
@@ -706,6 +708,24 @@
end;
+(* facts during goal refinement *)
+
+local
+
+fun gen_supply prep_att prep_fact args state =
+ state
+ |> assert_backward
+ |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+ (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
+
+in
+
+val supply = gen_supply (K I) (K I);
+val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
+
+end;
+
+
(* using/unfolding *)
local