put_thms: pass do_props;
authorwenzelm
Tue Mar 11 17:13:04 2008 +0100 (2008-03-11 ago)
changeset 2625096035b40be60
parent 26249 59ecf1ce8222
child 26251 b8c6259d366b
put_thms: pass do_props;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 10 21:51:47 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 11 17:13:04 2008 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4    val restore_naming: Proof.context -> Proof.context -> Proof.context
     1.5    val reset_naming: Proof.context -> Proof.context
     1.6    val hide_thms: bool -> string list -> Proof.context -> Proof.context
     1.7 -  val put_thms: string * thm list option -> Proof.context -> Proof.context
     1.8 +  val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
     1.9    val note_thmss: string ->
    1.10      ((bstring * attribute list) * (thmref * attribute list) list) list ->
    1.11        Proof.context -> (bstring * thm list) list * Proof.context
    1.12 @@ -877,8 +877,8 @@
    1.13          val index' = uncurry FactIndex.add_local opts (name, ths) index;
    1.14        in ((space', tab'), index') end);
    1.15  
    1.16 -fun put_thms thms ctxt =
    1.17 -  ctxt |> map_naming (K local_naming) |> update_thms (false, false) thms |> restore_naming ctxt;
    1.18 +fun put_thms do_props thms ctxt =
    1.19 +  ctxt |> map_naming (K local_naming) |> update_thms (do_props, false) thms |> restore_naming ctxt;
    1.20  
    1.21  
    1.22  (* note_thmss *)
    1.23 @@ -1071,7 +1071,7 @@
    1.24    in
    1.25      ctxt2
    1.26      |> auto_bind_facts (flat propss)
    1.27 -    |> put_thms (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
    1.28 +    |> put_thms false (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
    1.29      |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
    1.30    end;
    1.31