[isabelle-dev] is_concealed

[Florian Haftmann]

It had been a lapsus.  Regression is under way.

	Florian

On 26.11.2014 15:39, Florian Haftmann wrote:
> Hi Dmitriy,
> 
> thanks for figuring out.  I am currently having a look at it…
> 
> 	Florian
> 
> On 20.11.2014 17:34, Dmitriy Traytel wrote:
>> Sorry for reviving an ancient thread, but have the constants defined by
>> inductive ever been visible to find_consts since Florian's commit (I
>> presume 4a3747517552 ?).
>>
>> Today in be4a911aca71 (but also in Isabelle2014 and even in
>> Isabelle2012) in the following
>>
>> inductive xyz :: bool where "xyz"
>> find_consts name: xyz
>> ML ‹Consts.is_concealed (Sign.consts_of @{theory}) @{const_name xyz}›
>>
>> find_consts says "found nothing" and Consts.is_concealed says true.
>>
>> Visibility of constants is of course also important beyond find_consts,
>> e.g. for auto-completion.
>>
>> Dmitriy
>>
>> On 09.09.2010 09:57, Florian Haftmann wrote:
>>> Am 09.09.2010 09:15, schrieb Florian Haftmann:
>>>> Am 09.09.2010 09:02, schrieb Tobias Nipkow:
>>>>> Lars noticed an anomaly and Gerwin tracked it down:
>>>>> Command find_consts searches only for `visible' constants. Those defined
>>>>> by primrec and fun are visible, but those defined by inductive(_set) are
>>>>> concealed. It seems that the latter should be visible, too, right? If
>>>>> so, can somebody close to "inductive" fix that?
>>> Pushed.
>>>
>>> 	Florian
>>>
>>>
>>>
>>> _______________________________________________
>>> Isabelle-dev mailing list
>>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
# HG changeset patch
# Parent 8bcd656dec352f13b8c2241a3ac05b5485812864
do not conceal inductive predicate names properly, following 4a3747517552

diff -r 8bcd656dec35 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 26 15:35:28 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 26 15:43:50 2014 +0100
@@ -827,14 +827,15 @@
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
+    val is_auxiliary = length cs >= 2; 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> Local_Theory.conceal
+      |> is_auxiliary ? Local_Theory.conceal
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
+         ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> Local_Theory.restore_naming lthy;
+      ||> is_auxiliary ? Local_Theory.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
         (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141126/4e41efad/attachment.sig>