# HG changeset patch
# User blanchet
# Date 1282315488 -7200
# Node ID f7b32911340ba63a5025b2b92aeaea4ef45111cd
# Parent  d22c111837ad6490a0c05aff418e24764a4e97ad
unbreak "only" option of Sledgehammer

diff -r d22c111837ad -r f7b32911340b src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:44:48 2010 +0200
@@ -5,7 +5,7 @@
 
 header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
 
-theory NS_Shared imports Public begin
+theory NS_Shared imports Sledgehammer2d(*###*) Public begin
 
 text{*
 From page 247 of
@@ -311,6 +311,8 @@
       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
       Says B A (Crypt K (Nonce NB)) \<in> set evs"
 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+sledgehammer [atp = e, overlord] (Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
+apply (metis Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
 apply (analz_mono_contra, simp_all, blast)
 txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
     @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
diff -r d22c111837ad -r f7b32911340b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 16:44:48 2010 +0200
@@ -12,6 +12,8 @@
 
   val trace : bool Unsynchronized.ref
   val chained_prefix : string
+  val name_thms_pair_from_ref :
+    Proof.context -> thm list -> Facts.ref -> string * thm list
   val relevant_facts :
     bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> term list -> term
@@ -35,6 +37,14 @@
 (* Used to label theorems chained into the goal. *)
 val chained_prefix = sledgehammer_prefix ^ "chained_"
 
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+  let
+    val ths = ProofContext.get_fact ctxt xref
+    val name = Facts.string_of_ref xref
+               |> forall (member Thm.eq_thm chained_ths) ths
+                  ? prefix chained_prefix
+  in (name, ths) end
+
 
 (***************************************************************)
 (* Relevance Filtering                                         *)
@@ -565,7 +575,8 @@
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val axioms =
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
-          (if only then [] else all_name_thms_pairs ctxt add_thms chained_ths)
+          (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
+           else all_name_thms_pairs ctxt add_thms chained_ths)
       |> make_unique
       |> map (apsnd Clausifier.transform_elim_theorem)
       |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
diff -r d22c111837ad -r f7b32911340b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Fri Aug 20 16:44:48 2010 +0200
@@ -154,14 +154,6 @@
     handle ERROR msg => (NONE, "Error: " ^ msg)
   end
 
-fun name_thms_pair_from_ref ctxt chained_ths xref =
-  let
-    val ths = ProofContext.get_fact ctxt xref
-    val name = Facts.string_of_ref xref
-               |> forall (member Thm.eq_thm chained_ths) ths
-                  ? prefix chained_prefix
-  in (name, ths) end
-
 fun run_minimize params i refs state =
   let
     val ctxt = Proof.context_of state