# HG changeset patch
# User haftmann
# Date 1260782605 -3600
# Node ID 05cb31ca48ae7aaa8d931582661175eaa217c77b
# Parent  bb01fd325c6b0a327a28c2de75a89acabb6c1c25
explicit name for function space

diff -r bb01fd325c6b -r 05cb31ca48ae src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Dec 14 10:13:06 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Dec 14 10:23:25 2009 +0100
@@ -36,6 +36,7 @@
 signature CODE_THINGOL =
 sig
   include BASIC_CODE_THINGOL
+  val fun_tyco: string
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
@@ -388,8 +389,10 @@
    of SOME const' => (const', naming)
     | NONE => declare_const thy const naming;
 
+val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
+
 val unfold_fun = unfoldr
-  (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
+  (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
     | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
 
 end; (* local *)