# HG changeset patch
# User wenzelm
# Date 962310728 -7200
# Node ID 1f6f66fe777a550609369dc4e3ca3e086bd9447f
# Parent  29f1e53f993713c76febb8833a97d81c5267e00c
facts: handle multiple lists of arguments;

diff -r 29f1e53f9937 -r 1f6f66fe777a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jun 29 22:31:53 2000 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jun 29 22:32:08 2000 +0200
@@ -50,9 +50,11 @@
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
-  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 have_thmss: ((string * context attribute list) *
+    (thm list * context attribute list) list) list -> state -> state
+  val with_thmss: ((string * context attribute list) *
+    (thm list * context attribute list) list) list -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
   val assm: (int -> tactic) * (int -> tactic)
@@ -218,12 +220,10 @@
 
 val reset_facts = put_facts None;
 
-fun have_facts (name, facts) state =
+fun these_factss (state, named_factss) =
   state
-  |> put_facts (Some facts)
-  |> put_thms (name, facts);
-
-fun these_facts (state, ths) = have_facts ths state;
+  |> put_thmss named_factss
+  |> put_facts (Some (flat (map #2 named_factss)));
 
 
 (* goal *)
@@ -268,7 +268,7 @@
 fun assert_mode pred state =
   let val mode = get_mode state in
     if pred mode then state
-    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
+    else raise STATE ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode", state)
   end;
 
 fun is_chain state = get_mode state = ForwardChain;
@@ -466,15 +466,19 @@
 val let_bind_i = gen_bind (ProofContext.match_bind_i true);
 
 
-(* have_thmss *)
+(* have_thmss etc. *)
 
-fun have_thmss ths name atts ths_atts state =
+fun have_thmss args state =
   state
   |> assert_forward
-  |> map_context_result (ProofContext.have_thmss ths name atts ths_atts)
-  |> these_facts;
+  |> map_context_result (ProofContext.have_thmss args)
+  |> these_factss;
 
-fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
+fun simple_have_thms name thms = have_thmss [((name, []), [(thms, [])])];
+
+fun with_thmss args state =
+  let val state' = state |> have_thmss args
+  in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end;
 
 
 (* fix *)
@@ -498,9 +502,8 @@
   |> assert_forward
   |> map_context_result (f tac args)
   |> (fn (st, (factss, prems)) =>
-    foldl these_facts (st, factss)
-    |> put_thms ("prems", prems)
-    |> put_facts (Some (flat (map #2 factss))));
+    these_factss (st, factss)
+    |> put_thms ("prems", prems));
 
 val hard_asm_tac = Tactic.etac Drule.triv_goal;
 val soft_asm_tac = Tactic.rtac Drule.triv_goal
@@ -641,8 +644,8 @@
     print_result {kind = kind_name kind, name = name, thm = result};
     outer_state
     |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t]
-    |> have_thmss [] name atts [Thm.no_attributes
-        [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]]
+    |> have_thmss [((name, atts), [Thm.no_attributes
+        [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]])]
     |> opt_solve
     |> (Seq.flat o Seq.map after_qed)
   end;
diff -r 29f1e53f9937 -r 1f6f66fe777a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jun 29 22:31:53 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jun 29 22:32:08 2000 +0200
@@ -66,8 +66,9 @@
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
-  val have_thmss: thm list -> string -> context attribute list
-    -> (thm list * context attribute list) list -> context -> context * (string * thm list)
+  val have_thmss:
+    ((string * context attribute list) * (thm list * context attribute list) list) list ->
+      context -> context * (string * thm list) list
   val assume: ((int -> tactic) * (int -> tactic))
     -> (string * context attribute list * (string * (string list * string list)) list) list
     -> context -> context * ((string * thm list) list * thm list)
@@ -864,15 +865,17 @@
 
 (* have_thmss *)
 
-fun have_thmss more_ths name more_attrs ths_attrs ctxt =
+fun have_thss (ctxt, ((name, more_attrs), ths_attrs)) =
   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) @ more_ths;
+    val thms = flat (rev rev_thms);
   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
 
+fun have_thmss args ctxt = foldl_map have_thss (ctxt, args);
+
 
 
 (** assumptions **)
@@ -890,10 +893,10 @@
     val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
 
     val ths = map (fn th => ([th], [])) asms;
-    val (ctxt'', (_, thms)) =
+    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''