src/Pure/Isar/isar_syn.ML

 
 fun theorems kind = P.opt_locale_target -- P.name_facts
   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
 
 val theoremsP =
-  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
+  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
 
 val lemmasP =
-  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK);
+  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
     (P.opt_locale_target -- (P.and_list1 P.xthms1 >> flat)
       >> (fn (loc, args) => Toplevel.local_theory loc

       P.general_statement >> (fn ((loc, a), (elems, concl)) =>
       (Toplevel.print o
        Toplevel.local_theory_to_proof loc
          (Specification.theorem kind NONE (K I) a elems concl))));
 
-val theoremP = gen_theorem PureThy.theoremK;
-val lemmaP = gen_theorem PureThy.lemmaK;
-val corollaryP = gen_theorem PureThy.corollaryK;
+val theoremP = gen_theorem Thm.theoremK;
+val lemmaP = gen_theorem Thm.lemmaK;
+val corollaryP = gen_theorem Thm.corollaryK;
 
 val haveP =
   OuterSyntax.command "have" "state local goal"
     (K.tag_proof K.prf_goal)
     (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));