# HG changeset patch
# User blanchet
# Date 1396515084 -7200
# Node ID 5a93b8f928a29f7fe46530b5332e607daeff1148
# Parent  32e0da92c786262c9ca7487b4c9fe440f7adaac5
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes

diff -r 32e0da92c786 -r 5a93b8f928a2 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 03 10:51:22 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 03 10:51:24 2014 +0200
@@ -1315,7 +1315,22 @@
   val eq: T * T -> bool = op = o pairself T_of_bnf;
 );
 
-val bnf_interpretation = BNF_Interpretation.interpretation;
+fun with_repaired_path f bnf thy =
+  let
+    val qualifiers =
+      (case Binding.dest (name_of_bnf bnf) of
+        (* arbitrarily use "Fun" as prefix for "fun"*)
+        (_, [], @{type_name fun}) => [(Context.theory_name @{theory Fun}, false)]
+      | (_, qs, _) => qs)
+  in
+    thy
+    |> Sign.root_path
+    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
+    |> f bnf
+    |> Sign.restore_naming thy
+  end;
+
+val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
 
 fun register_bnf key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
diff -r 32e0da92c786 -r 5a93b8f928a2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 03 10:51:22 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 03 10:51:24 2014 +0200
@@ -190,7 +190,14 @@
   val eq: T * T -> bool = op = o pairself #T;
 );
 
-val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation;
+fun with_repaired_path f (fp_sugar as {T, ...} : fp_sugar) thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
+  |> f fp_sugar
+  |> Sign.restore_naming thy;
+
+val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
 
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
diff -r 32e0da92c786 -r 5a93b8f928a2 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:22 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:24 2014 +0200
@@ -158,7 +158,14 @@
   val eq: T * T -> bool = op = o pairself #ctrs;
 );
 
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation;
+fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
+  |> f ctr_sugar
+  |> Sign.restore_naming thy;
+
+val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
 
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}