src/Pure/Isar/local_theory.ML

 
 signature LOCAL_THEORY =
 sig
   val params_of: local_theory -> (string * typ) list
   val hyps_of: local_theory -> term list
-  val standard: local_theory -> thm -> thm
+  val standard: local_theory -> thm list -> thm list
   val pretty_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
   val quiet_mode: bool ref
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
   val theory: (theory -> theory) -> local_theory -> local_theory
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory

 val params_of = #params o Data.get;
 val hyps_of = #hyps o Data.get;
 
 fun standard ctxt =
   (case #locale (Data.get ctxt) of
-    NONE => Drule.standard
+    NONE => map Drule.standard
   | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt);
 
 
 (* print consts *)
 

 (* fact definitions *)
 
 fun notes kind facts ctxt =
   let
     val attrib = Attrib.attribute_i (ProofContext.theory_of ctxt);
-    val facts' = map (apsnd (map (apfst (map (standard ctxt))))) facts;
+    val facts' = map (apsnd (map (apfst (standard ctxt)))) facts;  (* FIXME burrow standard *)
   in
     ctxt |>
     (case locale_of ctxt of
       NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts'))
     | SOME (loc, _) =>