# HG changeset patch
# User wenzelm
# Date 1150565874 -7200
# Node ID 3f844845ecb890ddd9e6a7b9537d7c628261ec35
# Parent  4a3e35fd6e028b246ce142b4b85576a0a3060fd2
standard: simultaneous facts;

diff -r 4a3e35fd6e02 -r 3f844845ecb8 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jun 17 19:37:53 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Jun 17 19:37:54 2006 +0200
@@ -11,7 +11,7 @@
 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
@@ -75,7 +75,7 @@
 
 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);
 
 
@@ -210,7 +210,7 @@
 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