src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
changeset 62354 fdd6989cc8a0
parent 61259 6dc3d5d50e57
child 62552 53603d1aad5f
equal deleted inserted replaced
62341:a594429637fd 62354:fdd6989cc8a0
   167     else c
   167     else c
   168   end
   168   end
   169 fun alphanumerated_name prefix name =
   169 fun alphanumerated_name prefix name =
   170   prefix ^ (raw_explode #> map alphanumerate #> implode) name
   170   prefix ^ (raw_explode #> map alphanumerate #> implode) name
   171 
   171 
   172 (*SMLNJ complains if type annotation not used below*)
       
   173 fun mk_binding (config : config) ident =
   172 fun mk_binding (config : config) ident =
   174   let
   173   let
   175     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
   174     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
   176   in
   175   in
   177     case #problem_name config of
   176     case #problem_name config of