# HG changeset patch
# User wenzelm
# Date 930856857 -7200
# Node ID 4ae9c47f2b6bff5d0d0fd9c8c3d079f15713c383
# Parent  df31250ccb3a82d9a2d34fce08a21dd0145512a6
have_thmss: more_ths;
simple_have_thmss;

diff -r df31250ccb3a -r 4ae9c47f2b6b src/Pure/Isar/proof.ML
--- 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;