src/Pure/Isar/specification.ML
changeset 26345 f70620a4cf81
parent 26336 a0e2b706ce73
child 26595 855893d4d75f
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:48 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:49 2008 +0100
     1.3 @@ -213,18 +213,18 @@
     1.4  
     1.5  (* fact statements *)
     1.6  
     1.7 -fun gen_theorems prep_thms prep_att kind raw_facts lthy =
     1.8 +fun gen_theorems prep_fact prep_att kind raw_facts lthy =
     1.9    let
    1.10      val attrib = prep_att (ProofContext.theory_of lthy);
    1.11      val facts = raw_facts |> map (fn ((name, atts), bs) =>
    1.12        ((name, map attrib atts),
    1.13 -        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
    1.14 +        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
    1.15      val (res, lthy') = lthy |> LocalTheory.notes kind facts;
    1.16      val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
    1.17    in (res, lthy') end;
    1.18  
    1.19  val theorems = gen_theorems (K I) (K I);
    1.20 -val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
    1.21 +val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
    1.22  
    1.23  
    1.24  (* complex goal statements *)