simplified get_thm(s): back to plain name argument;
authorwenzelm
Thu Mar 20 00:20:48 2008 +0100 (2008-03-20 ago)
changeset 2634404dacc6809b6
parent 26343 0dd2eab7b296
child 26345 f70620a4cf81
simplified get_thm(s): back to plain name argument;
renamed former get_thms(_silent) to get_fact(_silent);
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Thu Mar 20 00:20:44 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Mar 20 00:20:48 2008 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  signature BASIC_PURE_THY =
     1.6  sig
     1.7 -  val get_thm: theory -> Facts.ref -> thm
     1.8 -  val get_thms: theory -> Facts.ref -> thm list
     1.9    structure ProtoPure:
    1.10      sig
    1.11        val thy: theory
    1.12 @@ -38,7 +36,10 @@
    1.13    val kind_internal: attribute
    1.14    val has_internal: Markup.property list -> bool
    1.15    val is_internal: thm -> bool
    1.16 -  val get_thms_silent: theory -> Facts.ref -> thm list
    1.17 +  val get_fact: theory -> Facts.ref -> thm list
    1.18 +  val get_fact_silent: theory -> Facts.ref -> thm list
    1.19 +  val get_thms: theory -> xstring -> thm list
    1.20 +  val get_thm: theory -> xstring -> thm
    1.21    val theorems_of: theory -> thm list NameSpace.table
    1.22    val all_facts_of: theory -> Facts.T
    1.23    val thms_of: theory -> (string * thm) list
    1.24 @@ -187,7 +188,7 @@
    1.25  fun show_result NONE = "none"
    1.26    | show_result (SOME (name, _)) = quote name;
    1.27  
    1.28 -fun get_fact silent theory thmref =
    1.29 +fun get silent theory thmref =
    1.30    let
    1.31      val name = Facts.name_of_ref thmref;
    1.32      val new_res = lookup_fact theory name;
    1.33 @@ -206,9 +207,11 @@
    1.34  
    1.35  in
    1.36  
    1.37 -val get_thms_silent = get_fact true;
    1.38 -val get_thms = get_fact false;
    1.39 -fun get_thm thy thmref = Facts.the_single (Facts.name_of_ref thmref) (get_thms thy thmref);
    1.40 +val get_fact_silent = get true;
    1.41 +val get_fact = get false;
    1.42 +
    1.43 +fun get_thms thy name = get_fact thy (Facts.Named (name, NONE));
    1.44 +fun get_thm thy name = Facts.the_single name (get_thms thy name);
    1.45  
    1.46  end;
    1.47  
    1.48 @@ -316,7 +319,7 @@
    1.49  
    1.50  in
    1.51  
    1.52 -fun note_thmss k = gen_note_thmss get_thms (kind k);
    1.53 +fun note_thmss k = gen_note_thmss get_fact (kind k);
    1.54  fun note_thmss_i k = gen_note_thmss (K I) (kind k);
    1.55  fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g);
    1.56