# HG changeset patch
# User wenzelm
# Date 1208360443 -7200
# Node ID fda7b0aff79835da25f4c78f52ade9156a59c4a4
# Parent  9f3f5429bac68b30b52bc86e5bd7ad9618dbe7ec
removed obsolete valid_thms;
removed obsolete premsN binding;
PureThy.get_fact: pass dynamic context;

diff -r 9f3f5429bac6 -r fda7b0aff798 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 16 17:40:42 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 16 17:40:43 2008 +0200
@@ -95,7 +95,6 @@
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
-  val valid_thms: Proof.context -> string * thm list -> bool
   val add_path: string -> Proof.context -> Proof.context
   val no_base_names: Proof.context -> Proof.context
   val qualified_names: Proof.context -> Proof.context
@@ -793,14 +792,14 @@
 
 local
 
-fun retrieve_thms _ pick ctxt (Facts.Fact s) =
+fun retrieve_thms pick ctxt (Facts.Fact s) =
       let
         val prop = Syntax.read_prop (set_mode mode_default ctxt) s
           |> singleton (Variable.polymorphic ctxt);
         val th = Goal.prove ctxt [] [] prop (K (ALLGOALS (some_fact_tac ctxt)))
           handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
       in pick "" [th] end
-  | retrieve_thms from_thy pick ctxt xthmref =
+  | retrieve_thms pick ctxt xthmref =
       let
         val thy = theory_of ctxt;
         val local_facts = facts_of ctxt;
@@ -811,29 +810,20 @@
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
               SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
-            | NONE => from_thy thy xthmref);
+            | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
 
 in
 
-val get_fact = retrieve_thms PureThy.get_fact (K I);
-val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
+val get_fact = retrieve_thms (K I);
+val get_fact_single = retrieve_thms Facts.the_single;
 
-fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
 
 end;
 
 
-(* valid_thms *)
-
-fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_thms_silent ctxt name) () of
-    NONE => false
-  | SOME ths' => Thm.eq_thms (ths, ths'));
-
-
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
@@ -1041,7 +1031,6 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> put_thms false (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
     |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;