[isabelle-dev] Thn.dest_arg

[Florian Haftmann]

Call me stupid, but I don't see any difference between the following two
function definitions in Pure/thm.ML:

> fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
>       let val A = Term.argument_type_of c 0
>       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
>   | dest_arg ct = raise CTERM ("dest_arg", [ct]);
> 
> fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) =
>       let val A = Term.argument_type_of c 0
>       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
>   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);

Any idea that to do about this?

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
Url : https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080523/e7b121dc/attachment.vcf 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
Url : https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080523/e7b121dc/attachment.pgp