Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
P.locale_element;
authorwenzelm
Wed, 09 Nov 2005 16:26:45 +0100
changeset 18130 108ed679cf5a
parent 18129 62adfb6a7060
child 18131 8c3089df74ba
P.locale_element;
src/Pure/proof_general.ML file | annotate | diff | comparison | revisions 
--- 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 ":" --|
isabelle