# 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