explicit name for function space
authorhaftmann
Mon Dec 14 10:23:25 2009 +0100 (2009-12-14)
changeset 3408405cb31ca48ae
parent 34081 bb01fd325c6b
child 34085 420234017d39
explicit name for function space
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Dec 14 10:13:06 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Dec 14 10:23:25 2009 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4  signature CODE_THINGOL =
     1.5  sig
     1.6    include BASIC_CODE_THINGOL
     1.7 +  val fun_tyco: string
     1.8    val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
     1.9    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
    1.10    val unfold_fun: itype -> itype list * itype
    1.11 @@ -388,8 +389,10 @@
    1.12     of SOME const' => (const', naming)
    1.13      | NONE => declare_const thy const naming;
    1.14  
    1.15 +val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
    1.16 +
    1.17  val unfold_fun = unfoldr
    1.18 -  (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
    1.19 +  (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
    1.20      | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
    1.21  
    1.22  end; (* local *)