# HG changeset patch
# User wenzelm
# Date 1131550005 -3600
# Node ID 108ed679cf5a4e3b38d80d270a8ea3913f85dce7
# Parent  62adfb6a706069de29591be63fdcf62f585ebddb
P.locale_element;

diff -r 62adfb6a7060 -r 108ed679cf5a src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Nov 09 16:26:44 2005 +0100
+++ b/src/Pure/proof_general.ML	Wed Nov 09 16:26:45 2005 +0100
@@ -881,7 +881,7 @@
             (* see isar_syn.ML/gen_theorem *)
          val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
          val general_statement =
-            statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
+            statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
 
             val gen_theoremP =
                 P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|