[isabelle] Isabelle2004 proofterm bug/failure



Hello,

When I run the following function on the theorem "Product_Type.split_comp_eq"
I get an exception

*** Non-unifiable types:
*** ?'t27 => ?'t26
***
*** 'a => 'd

This does not happen to any of the thousands of other theorems I've tried it on, so I figure it must be some minor bug in the reconstruction algorithm (though
I'm frequently blaming my mistakes on others)

  fun proof_of_thm thm =
      let
        val {prop, der=(_, prf), sign, ...} = rep_thm thm
val prf' = Reconstruct.reconstruct_proof sign prop (Proofterm.strip_thm prf)
        val prf'' = Reconstruct.expand_proof sign [("", None)] prf'
      in
        prf''
      end

Best,

Sean







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