# HG changeset patch
# User wenzelm
# Date 1081880471 -7200
# Node ID b9cd48af3512e3b18f38478ab3b2411f7a3ab8fb
# Parent  4740fc2da7bbb49a1dfb1e5dd974096066f68736
export put_thms;
do not export use_facts, reset_facts;

diff -r 4740fc2da7bb -r b9cd48af3512 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 13 13:53:54 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 13 20:21:11 2004 +0200
@@ -26,13 +26,12 @@
   val sign_of: state -> Sign.sg
   val map_context: (context -> context) -> state -> state
   val warn_extra_tfrees: state -> state -> state
+  val put_thms: string * thm list -> state -> state
   val reset_thms: string -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val get_goal: state -> context * (thm list * thm)
   val goal_facts: (state -> thm list) -> state -> state
-  val use_facts: state -> state
-  val reset_facts: state -> state
   val get_mode: state -> mode
   val is_chain: state -> bool
   val assert_forward: state -> state