diff -r 54ae6c6ef3b1 -r 2550a5578d39 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -88,13 +88,13 @@
   val invoke_case: string * string option list * context attribute list -> state -> state
   val multi_theorem: string
     -> (xstring * (context attribute list * context attribute list list)) option
-    -> bstring * theory attribute list -> context attribute Locale.element list
+    -> bstring * theory attribute list -> context attribute Locale.elem_or_expr list
     -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
     -> theory -> state
   val multi_theorem_i: string
     -> (string * (context attribute list * context attribute list list)) option
     -> bstring * theory attribute list
-    -> context attribute Locale.element_i list
+    -> context attribute Locale.elem_or_expr_i list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> theory -> state
   val chain: state -> state