# HG changeset patch # User blanchet # Date 1392190556 -3600 # Node ID 91bc9f69a95835492e143ab0a4cd17b250a7ffd6 # Parent 4e79187f847e352d7098158a2900a5004d5ec8e3 got rid of dynamic scoping the easy way diff -r 4e79187f847e -r 91bc9f69a958 src/HOL/Tools/Function/function_core.ML --- 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