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.
Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
authorwenzelm
Fri, 15 Jul 2011 16:51:01 +0200
changeset 43842 f035d867fb41
parent 43841 60cd0ac63fdb
child 43843 16f2fd9103bd
Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
src/Pure/Isar/element.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/element.ML	Fri Jul 15 14:07:12 2011 +0200
+++ b/src/Pure/Isar/element.ML	Fri Jul 15 16:51:01 2011 +0200
@@ -526,7 +526,7 @@
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
-   {binding = tap (fn b => if Binding.is_empty b then "" else Variable.check_name b),
+   {binding = I,
     typ = I,
     term = I,
     pattern = I,
isabelle