[isabelle] string -> const



Hello,

Is there a way to go from a string to a const without incurring error messages?
EG.  Right now I have:

fun type_of_const c = type_of (read c) handle _ => type_of (read ("op " ^ c))

but I get a bunch of cruft when it's an op, like "==>".

(The "==>" lives in the proof term)

Thanks,

Sean





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.