[isabelle-dev] fun : term -> string

[Jasmin Christian Blanchette]

Am 23.09.2010 um 16:11 schrieb Makarius:

>> I found a couple of ad hoc solutions to this problem. One way is to set the print mode to "input":
>> 
>>   Print_Mode.setmp (Print_Mode.input ::
>>       filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
>>       (Syntax.string_of_term ctxt) @{term "str"}
> 
> Note that the Print_Mode.input never has any effect on output, it is filtered out from the print_mode_value.  So there is no point of adding it to the list.

Indeed.

>> The business with filter is there to respect the user's "xsymbols" preference. You probably don't need it.
> 
> There might be more user preferences that are getting lost here.  Under normal circumstances the default print mode should not be filtered.

But something has to be filtered away, otherwise one gets YXML.

For the record: What I'm trying to do is to take a nameless fact and produce a `foo` string out of it, hoping that this might work (and if it doesn't, hoping the user is smart enough to find out which fact Sledgehammer was trying to refer to and repair or name it).

Jasmin