src/Pure/Isar/isar_syn.ML

       >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
 
 
 (* theorems *)
 
-val theorems =
-  Parse_Spec.name_facts -- Parse.for_fixes
-    >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes);
-
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems" theorems;
-
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" theorems;
+val _ =
+  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
+    (Parse_Spec.name_facts -- Parse.for_fixes >>
+      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
     (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>

           Thm.theoremK NONE (K I) a includes elems concl)));
 
 val _ = theorem @{command_keyword theorem} false "theorem";
 val _ = theorem @{command_keyword lemma} false "lemma";
 val _ = theorem @{command_keyword corollary} false "corollary";
-val _ = theorem @{command_keyword schematic_theorem} true "schematic goal";
-val _ = theorem @{command_keyword schematic_lemma} true "schematic goal";
-val _ = theorem @{command_keyword schematic_corollary} true "schematic goal";
+val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
 
 
 val structured_statement =
   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
     >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));