src/Tools/code/code_thingol.ML
changeset 31054 841c9f67f9e7
parent 31049 396d4d6a1594
child 31063 88aaab83b6fc
     1.1 --- a/src/Tools/code/code_thingol.ML	Wed May 06 19:09:14 2009 +0200
     1.2 +++ b/src/Tools/code/code_thingol.ML	Wed May 06 19:09:14 2009 +0200
     1.3 @@ -61,6 +61,7 @@
     1.4    val lookup_tyco: naming -> string -> string option
     1.5    val lookup_instance: naming -> class * string -> string option
     1.6    val lookup_const: naming -> string -> string option
     1.7 +  val ensure_declared_const: theory -> string -> naming -> string * naming
     1.8  
     1.9    datatype stmt =
    1.10        NoStmt
    1.11 @@ -359,6 +360,11 @@
    1.12  fun declare_const thy = declare thy map_const
    1.13    lookup_const Symtab.update_new namify_const;
    1.14  
    1.15 +fun ensure_declared_const thy const naming =
    1.16 +  case lookup_const naming const
    1.17 +   of SOME const' => (const', naming)
    1.18 +    | NONE => declare_const thy const naming;
    1.19 +
    1.20  val unfold_fun = unfoldr
    1.21    (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
    1.22      | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)