# HG changeset patch
# User wenzelm
# Date 930856827 -7200
# Node ID df31250ccb3a82d9a2d34fce08a21dd0145512a6
# Parent  747f656e04ec0923967d087952258493211e1ae6
have_thmss: more_ths;

diff -r 747f656e04ec -r df31250ccb3a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jul 01 21:19:45 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 01 21:20:27 1999 +0200
@@ -44,7 +44,7 @@
   val put_thm: string * thm -> context -> context
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
-  val have_thmss: string -> context attribute list
+  val have_thmss: thm list -> string -> context attribute list
     -> (thm list * context attribute list) list -> context -> context * (string * thm list)
   val assumptions: context -> (cterm * (int -> tactic)) list
   val fixed_names: context -> string list
@@ -617,13 +617,13 @@
 
 (* have_thmss *)
 
-fun have_thmss name more_attrs ths_attrs ctxt =
+fun have_thmss more_ths name more_attrs ths_attrs ctxt =
   let
     fun app ((ct, ths), (th, attrs)) =
       let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
       in (ct', th' :: ths) end
     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
-    val thms = flat (rev rev_thms);
+    val thms = flat (rev rev_thms) @ more_ths;
   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
 
 
@@ -654,7 +654,7 @@
     val (ctxt'', (_, thms)) =
       ctxt'
       |> auto_bind_facts name props
-      |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
+      |> have_thmss [] name (attrs @ [Drule.tag_assumption]) ths;
 
     val ctxt''' =
       ctxt''