# HG changeset patch
# User wenzelm
# Date 1205968851 -3600
# Node ID 17debd2fff8e564c825a0f8959758a7a245ac0ad
# Parent  f70620a4cf8110bc1155cd806c11680912d3783d
simplified get_thm(s): back to plain name argument;
renamed former get_thm to get_fact_single, and get_thms to get_fact;

diff -r f70620a4cf81 -r 17debd2fff8e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 20 00:20:49 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 20 00:20:51 2008 +0100
@@ -91,8 +91,10 @@
     -> Proof.context * (term list list * (Proof.context -> Proof.context))
   val fact_tac: thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
-  val get_thm: Proof.context -> Facts.ref -> thm
-  val get_thms: Proof.context -> Facts.ref -> thm list
+  val get_fact: Proof.context -> Facts.ref -> thm list
+  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
@@ -812,15 +814,19 @@
             | NONE => from_thy thy xthmref);
       in pick name thms end;
 
-val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
-val get_thms = retrieve_thms PureThy.get_thms (K I);
-val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
+val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
+
+val get_fact = retrieve_thms PureThy.get_fact (K I);
+val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
+
+fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
+fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
 
 
 (* valid_thms *)
 
 fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
+  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
 
@@ -859,7 +865,7 @@
 
 in
 
-fun note_thmss k = gen_note_thmss get_thms k;
+fun note_thmss k = gen_note_thmss get_fact k;
 fun note_thmss_i k = gen_note_thmss (K I) k;
 
 end;
diff -r f70620a4cf81 -r 17debd2fff8e src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 00:20:49 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 00:20:51 2008 +0100
@@ -264,8 +264,8 @@
 
 (** fact references **)
 
-fun thm name = ProofContext.get_thm (the_local_context ()) (Facts.Named (name, NONE));
-fun thms name = ProofContext.get_thms (the_local_context ()) (Facts.Named (name, NONE));
+fun thm name = ProofContext.get_thm (the_local_context ()) name;
+fun thms name = ProofContext.get_thms (the_local_context ()) name;
 
 
 local
@@ -280,15 +280,15 @@
     ML_Syntax.print_pair ML_Syntax.print_string
       (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
 
-fun thm_antiq kind = value_antiq kind
+fun thm_antiq name get = value_antiq name
   (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
-    "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
+    get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
 
 in
 
 val _ = add_keywords ["(", ")", "-", ","];
-val _ = thm_antiq "thm";
-val _ = thm_antiq "thms";
+val _ = thm_antiq "thm" "ProofContext.get_fact_single";
+val _ = thm_antiq "thms" "ProofContext.get_fact";
 
 end;