renamed former get_thms(_silent) to get_fact(_silent);
authorwenzelm
Thu Mar 20 00:20:49 2008 +0100 (2008-03-20)
changeset 26345f70620a4cf81
parent 26344 04dacc6809b6
child 26346 17debd2fff8e
renamed former get_thms(_silent) to get_fact(_silent);
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 20 00:20:48 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Mar 20 00:20:49 2008 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4  fun gen_thm pick = Scan.depend (fn context =>
     1.5    let
     1.6      val thy = Context.theory_of context;
     1.7 -    val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
     1.8 +    val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
     1.9      fun get_fact s = get (Facts.Fact s);
    1.10      fun get_named s = get (Facts.Named (s, NONE));
    1.11    in
     2.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 20 00:20:48 2008 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 20 00:20:49 2008 +0100
     2.3 @@ -1407,7 +1407,7 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
     2.8 +fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
     2.9  fun cert_facts x = prep_facts I (K I) (K I) x;
    2.10  
    2.11  end;
     3.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:48 2008 +0100
     3.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:49 2008 +0100
     3.3 @@ -213,18 +213,18 @@
     3.4  
     3.5  (* fact statements *)
     3.6  
     3.7 -fun gen_theorems prep_thms prep_att kind raw_facts lthy =
     3.8 +fun gen_theorems prep_fact prep_att kind raw_facts lthy =
     3.9    let
    3.10      val attrib = prep_att (ProofContext.theory_of lthy);
    3.11      val facts = raw_facts |> map (fn ((name, atts), bs) =>
    3.12        ((name, map attrib atts),
    3.13 -        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
    3.14 +        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
    3.15      val (res, lthy') = lthy |> LocalTheory.notes kind facts;
    3.16      val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
    3.17    in (res, lthy') end;
    3.18  
    3.19  val theorems = gen_theorems (K I) (K I);
    3.20 -val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
    3.21 +val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
    3.22  
    3.23  
    3.24  (* complex goal statements *)