simplified get_thm(s): back to plain name argument;
authorwenzelm
Thu Mar 20 00:20:51 2008 +0100 (2008-03-20 ago)
changeset 2634617debd2fff8e
parent 26345 f70620a4cf81
child 26347 105f55201077
simplified get_thm(s): back to plain name argument;
renamed former get_thm to get_fact_single, and get_thms to get_fact;
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 20 00:20:49 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 20 00:20:51 2008 +0100
     1.3 @@ -91,8 +91,10 @@
     1.4      -> Proof.context * (term list list * (Proof.context -> Proof.context))
     1.5    val fact_tac: thm list -> int -> tactic
     1.6    val some_fact_tac: Proof.context -> int -> tactic
     1.7 -  val get_thm: Proof.context -> Facts.ref -> thm
     1.8 -  val get_thms: Proof.context -> Facts.ref -> thm list
     1.9 +  val get_fact: Proof.context -> Facts.ref -> thm list
    1.10 +  val get_fact_single: Proof.context -> Facts.ref -> thm
    1.11 +  val get_thms: Proof.context -> xstring -> thm list
    1.12 +  val get_thm: Proof.context -> xstring -> thm
    1.13    val valid_thms: Proof.context -> string * thm list -> bool
    1.14    val add_path: string -> Proof.context -> Proof.context
    1.15    val no_base_names: Proof.context -> Proof.context
    1.16 @@ -812,15 +814,19 @@
    1.17              | NONE => from_thy thy xthmref);
    1.18        in pick name thms end;
    1.19  
    1.20 -val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
    1.21 -val get_thms = retrieve_thms PureThy.get_thms (K I);
    1.22 -val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
    1.23 +val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
    1.24 +
    1.25 +val get_fact = retrieve_thms PureThy.get_fact (K I);
    1.26 +val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
    1.27 +
    1.28 +fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
    1.29 +fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
    1.30  
    1.31  
    1.32  (* valid_thms *)
    1.33  
    1.34  fun valid_thms ctxt (name, ths) =
    1.35 -  (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
    1.36 +  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
    1.37      NONE => false
    1.38    | SOME ths' => Thm.eq_thms (ths, ths'));
    1.39  
    1.40 @@ -859,7 +865,7 @@
    1.41  
    1.42  in
    1.43  
    1.44 -fun note_thmss k = gen_note_thmss get_thms k;
    1.45 +fun note_thmss k = gen_note_thmss get_fact k;
    1.46  fun note_thmss_i k = gen_note_thmss (K I) k;
    1.47  
    1.48  end;
     2.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 20 00:20:49 2008 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 00:20:51 2008 +0100
     2.3 @@ -264,8 +264,8 @@
     2.4  
     2.5  (** fact references **)
     2.6  
     2.7 -fun thm name = ProofContext.get_thm (the_local_context ()) (Facts.Named (name, NONE));
     2.8 -fun thms name = ProofContext.get_thms (the_local_context ()) (Facts.Named (name, NONE));
     2.9 +fun thm name = ProofContext.get_thm (the_local_context ()) name;
    2.10 +fun thms name = ProofContext.get_thms (the_local_context ()) name;
    2.11  
    2.12  
    2.13  local
    2.14 @@ -280,15 +280,15 @@
    2.15      ML_Syntax.print_pair ML_Syntax.print_string
    2.16        (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
    2.17  
    2.18 -fun thm_antiq kind = value_antiq kind
    2.19 +fun thm_antiq name get = value_antiq name
    2.20    (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
    2.21 -    "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
    2.22 +    get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
    2.23  
    2.24  in
    2.25  
    2.26  val _ = add_keywords ["(", ")", "-", ","];
    2.27 -val _ = thm_antiq "thm";
    2.28 -val _ = thm_antiq "thms";
    2.29 +val _ = thm_antiq "thm" "ProofContext.get_fact_single";
    2.30 +val _ = thm_antiq "thms" "ProofContext.get_fact";
    2.31  
    2.32  end;
    2.33