[isabelle-dev] Typing problem in autogenerated axiom

[Andreas Schropp]

Andreas Schropp wrote:
> Let me put this into perspective, in the light of a forthcoming kernel 
> extension/modification:
>  in this kernel patch, all sort constaints and type class reasoning 
> steps are eliminated in proofterms on theorem boundaries, and strip_sorted

Sorry, I mean unconstrained variants of axioms, e.g.
  OFCLASS(?'a::{}, type) ==> (?t::?'a::{})=?t
for HOL reflexivity.

> variants of the axioms are asserted on the proofterm side. So what 
> remains is a proof which sort and typeclass reasoning internalized 
> into the logic.
> From my POV this is needed to translate HOL into logics not involving 
> Isabelle-style type classes.