--- 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