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.
got rid of dynamic scoping the easy way
authorblanchet
Wed, 12 Feb 2014 08:35:56 +0100
changeset 55396 91bc9f69a958
parent 55395 4e79187f847e
child 55397 c2506f61fd26
got rid of dynamic scoping the easy way
src/HOL/Tools/Function/function_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/function_core.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -829,7 +829,7 @@
   let
     val FunctionConfig {domintros, default=default_opt, ...} = config
 
-    val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
+    val default_str = the_default "%x. HOL.undefined" default_opt
     val fvar = Free (fname, fT)
     val domT = domain_type fT
     val ranT = range_type fT
isabelle