src/Pure/codegen.ML
changeset 14769 b698d0b243dc
parent 14598 7009f59711e3
child 14818 ad83019a66a4
equal deleted inserted replaced
14768:68496ae66405 14769:b698d0b243dc
   234        Some T =>
   234        Some T =>
   235          let val T' = (case tyopt of
   235          let val T' = (case tyopt of
   236                 None => T
   236                 None => T
   237               | Some ty =>
   237               | Some ty =>
   238                   let val U = prep_type sg ty
   238                   let val U = prep_type sg ty
   239                   in if Type.typ_instance (Sign.tsig_of sg, U, T) then U
   239                   in if Sign.typ_instance sg (U, T) then U
   240                     else error ("Illegal type constraint for constant " ^ cname)
   240                     else error ("Illegal type constraint for constant " ^ cname)
   241                   end)
   241                   end)
   242          in (case assoc (consts, (cname, T')) of
   242          in (case assoc (consts, (cname, T')) of
   243              None => CodegenData.put {codegens = codegens,
   243              None => CodegenData.put {codegens = codegens,
   244                tycodegens = tycodegens,
   244                tycodegens = tycodegens,
   312 
   312 
   313 
   313 
   314 (**** retrieve definition of constant ****)
   314 (**** retrieve definition of constant ****)
   315 
   315 
   316 fun is_instance thy T1 T2 =
   316 fun is_instance thy T1 T2 =
   317   Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2);
   317   Sign.typ_instance (sign_of thy) (T1, Type.varifyT T2);
   318 
   318 
   319 fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) =>
   319 fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) =>
   320   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   320   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   321 
   321 
   322 fun get_defn thy s T =
   322 fun get_defn thy s T =