[isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore

[Florian Haftmann]

I have done a grep on this:

> src/Pure/Isar/named_target.ML:197:      (Context.Proof o Local_Theory.restore, lthy)
> src/HOL/Library/bnf_axiomatization.ML:84:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_def.ML:794:        ? Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_fp_n2m.ML:397:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_fp_def_sugar.ML:1224:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_fp_def_sugar.ML:2123:          ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:306:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:384:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:531:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:654:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:735:            ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:836:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:874:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:907:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:973:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1016:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1060:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1333:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1378:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1468:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1541:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_gfp.ML:1736:          ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_util.ML:151:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:255:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:334:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:473:            ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:659:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:770:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:927:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:977:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:1084:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:1154:      ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp.ML:1411:                ||> `Local_Theory.restore;
> src/HOL/Tools/BNF/bnf_lfp_size.ML:191:        ||> `Local_Theory.restore;
> src/HOL/Tools/Transfer/transfer_bnf.ML:300:    |> Local_Theory.restore
> src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML:503:      ||> `Local_Theory.restore;
> src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML:633:            ||> `Local_Theory.restore;

It seems feasible to get rid of the misleading Local_Theory.restore in
HOL tools.  The remaining occurence in src/Pure/Isar/named_target.ML is
one special case which would remain to be inspected then.  I guess it
will end up similary like the infamous Local_Theory.reinit, i.e.
disappear in the long run.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150412/55d486ae/attachment.sig>