--- a/src/Pure/Isar/proof.ML Thu Jul 01 21:20:27 1999 +0200
+++ b/src/Pure/Isar/proof.ML Thu Jul 01 21:20:57 1999 +0200
@@ -31,8 +31,9 @@
val bind_i: (indexname * term) list -> state -> state
val match_bind: (string list * string) list -> state -> state
val match_bind_i: (term list * term) list -> state -> state
- val have_thmss: string -> context attribute list ->
+ val have_thmss: thm list -> string -> context attribute list ->
(thm list * context attribute list) list -> state -> state
+ val simple_have_thms: string -> thm list -> state -> state
val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
-> state -> state
val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
@@ -436,12 +437,14 @@
(* have_thmss *)
-fun have_thmss name atts ths_atts state =
+fun have_thmss ths name atts ths_atts state =
state
|> assert_forward
- |> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts)
+ |> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts)
|> these_facts;
+fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
+
(* fix *)
@@ -619,7 +622,7 @@
state
|> close_block
|> auto_bind_facts name [t]
- |> have_thmss name atts [Thm.no_attributes [result]]
+ |> have_thmss [] name atts [Thm.no_attributes [result]]
|> opt_solve
end;