[isabelle-dev] Thn.dest_arg

[Stefan Berghofer]

Florian Haftmann wrote:
> 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?

The functions only differ in the pattern "t = ..." in the first line.
Given a function applied to one argument, dest_arg returns this argument.
In contrast, given a function applied to two arguments, dest_arg1 returns
the *first* of these arguments, while dest_arg would return the second one.

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe