diff -r 04dacc6809b6 -r f70620a4cf81 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:48 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 20 00:20:49 2008 +0100
@@ -213,18 +213,18 @@
 
 (* fact statements *)
 
-fun gen_theorems prep_thms prep_att kind raw_facts lthy =
+fun gen_theorems prep_fact prep_att kind raw_facts lthy =
   let
     val attrib = prep_att (ProofContext.theory_of lthy);
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
-        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
+        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     val (res, lthy') = lthy |> LocalTheory.notes kind facts;
     val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
-val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
+val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
 
 
 (* complex goal statements *)