have_thmss: more_ths;
authorwenzelm
Thu Jul 01 21:20:27 1999 +0200 (1999-07-01)
changeset 6875df31250ccb3a
parent 6874 747f656e04ec
child 6876 4ae9c47f2b6b
have_thmss: more_ths;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jul 01 21:19:45 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jul 01 21:20:27 1999 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4    val put_thm: string * thm -> context -> context
     1.5    val put_thms: string * thm list -> context -> context
     1.6    val put_thmss: (string * thm list) list -> context -> context
     1.7 -  val have_thmss: string -> context attribute list
     1.8 +  val have_thmss: thm list -> string -> context attribute list
     1.9      -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    1.10    val assumptions: context -> (cterm * (int -> tactic)) list
    1.11    val fixed_names: context -> string list
    1.12 @@ -617,13 +617,13 @@
    1.13  
    1.14  (* have_thmss *)
    1.15  
    1.16 -fun have_thmss name more_attrs ths_attrs ctxt =
    1.17 +fun have_thmss more_ths name more_attrs ths_attrs ctxt =
    1.18    let
    1.19      fun app ((ct, ths), (th, attrs)) =
    1.20        let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
    1.21        in (ct', th' :: ths) end
    1.22      val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
    1.23 -    val thms = flat (rev rev_thms);
    1.24 +    val thms = flat (rev rev_thms) @ more_ths;
    1.25    in (ctxt' |> put_thms (name, thms), (name, thms)) end;
    1.26  
    1.27  
    1.28 @@ -654,7 +654,7 @@
    1.29      val (ctxt'', (_, thms)) =
    1.30        ctxt'
    1.31        |> auto_bind_facts name props
    1.32 -      |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
    1.33 +      |> have_thmss [] name (attrs @ [Drule.tag_assumption]) ths;
    1.34  
    1.35      val ctxt''' =
    1.36        ctxt''