# HG changeset patch
# User wenzelm
# Date 1205252021 -3600
# Node ID b8c6259d366bdfac3d9e0a41530781c076069aac
# Parent  96035b40be60246434bd4b2e6b7a8dc8719f887f
put_facts: do_props, i.e. facts are indexed by proposition again;

diff -r 96035b40be60 -r b8c6259d366b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Mar 11 17:13:04 2008 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 11 17:13:41 2008 +0100
@@ -18,7 +18,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val add_binds_i: (indexname * term option) list -> state -> state
-  val put_thms: string * thm list option -> state -> state
+  val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val put_facts: thm list option -> state -> state
@@ -199,7 +199,7 @@
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
 val add_binds_i = map_context o ProofContext.add_binds_i;
-val put_thms = map_context o ProofContext.put_thms;
+val put_thms = map_context oo ProofContext.put_thms;
 
 
 (* facts *)
@@ -216,7 +216,7 @@
 
 fun put_facts facts =
   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  put_thms (AutoBind.thisN, facts);
+  put_thms true (AutoBind.thisN, facts);
 
 fun these_factss more_facts (named_factss, state) =
   (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));