Re: [isabelle] Strange interaction between Rewrite and Adhoc_Overloading



On 02/05/18 11:00, Christian Sternagel wrote:
> 
> The easy fix would be to add (but I didn't do anything in the repo,
> because I wanted to avoid potential clashes with others).
> 
>   hide_const (open) List.nth
> 
> at the top of Definedness.thy. The problem was just that we define our
> own "nth" (in Data_List) function but since "nth" is also defined in
> Main and Definedness imports Adhoc_Overloading after Data_List. No
> suddenly "nth" referred to List.nth instead of Data_List.nth.

There are further hide commands that getoverridden by the merge with
Main from the right. This is another example of merge fragility.

I have now clarified the imports as in the included changeset.


	Makarius
# HG changeset patch
# User wenzelm
# Date 1525252310 -7200
#      Wed May 02 11:11:50 2018 +0200
# Node ID d60436a866bb50ffbfc98598abd24160fdd37df6
# Parent  d458a5cbda540b83c0d9920642c6e74bc8e5315d
clarified imports for the sake of "hide_const (open) List.nth";

diff -r d458a5cbda54 -r d60436a866bb thys/HOLCF-Prelude/Definedness.thy
--- a/thys/HOLCF-Prelude/Definedness.thy	Wed May 02 10:49:26 2018 +0200
+++ b/thys/HOLCF-Prelude/Definedness.thy	Wed May 02 11:11:50 2018 +0200
@@ -3,7 +3,6 @@
 theory Definedness
   imports
     Data_List
-    "HOL-Library.Adhoc_Overloading"
 begin
 
 text \<open>
diff -r d458a5cbda54 -r d60436a866bb thys/HOLCF-Prelude/HOLCF_Main.thy
--- a/thys/HOLCF-Prelude/HOLCF_Main.thy	Wed May 02 10:49:26 2018 +0200
+++ b/thys/HOLCF-Prelude/HOLCF_Main.thy	Wed May 02 11:11:50 2018 +0200
@@ -4,6 +4,7 @@
   imports
     HOLCF
     "HOLCF-Library.Int_Discrete"
+    "HOL-Library.Adhoc_Overloading"
 begin
 
 text \<open>


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.