# HG changeset patch
# User traytel
# Date 1456909332 -3600
# Node ID 5b5b704f4811c3bf6e554d4508bb88dfa3e0cac7
# Parent  f187aaf602c4f9cc29a010d5b71b1fade062f1f4
respect qualification when noting theorems in prim(co)rec

diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 02 10:01:31 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 02 10:02:12 2016 +0100
@@ -1098,6 +1098,7 @@
     val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts);
 
     val fun_names = map Binding.name_of bs;
+    val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs;
     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
     val frees = map (fst #>> Binding.name_of #> Free) fixes;
     val has_call = Term.exists_subterm (member (op =) frees);
@@ -1520,6 +1521,7 @@
         val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
 
         val common_name = mk_common_name fun_names;
+        val common_qualify = fold_rev I qualifys;
 
         val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
@@ -1532,7 +1534,8 @@
            (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coinduct_attrs)]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
-            ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
+            ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs),
+              [(thms, [])]));
 
         val notes =
           [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
@@ -1547,9 +1550,10 @@
            (selN, sel_thmss, simp_attrs),
            (simpsN, simp_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
-            map2 (fn fun_name => fn thms =>
-                ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
-              fun_names (take actual_nn thmss))
+            @{map 3} (fn fun_name => fn qualify => fn thms =>
+                ((qualify (Binding.qualify true fun_name (Binding.name thmN)), attrs),
+                  [(thms, [])]))
+              fun_names qualifys (take actual_nn thmss))
           |> filter_out (null o fst o hd o snd);
 
         val fun_ts0 = map fst def_infos;
diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Mar 02 10:01:31 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Mar 02 10:02:12 2016 +0100
@@ -537,7 +537,8 @@
 val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec;
 val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global;
 val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded;
-val primrec_simple = apfst (apsnd (old_of_new (flat o snd))) ooo BNF_LFP_Rec_Sugar.primrec_simple;
+val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo
+  BNF_LFP_Rec_Sugar.primrec_simple;
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword datatype_compat}
diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Mar 02 10:01:31 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Mar 02 10:02:12 2016 +0100
@@ -73,7 +73,8 @@
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
   val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory ->
-    (string list * (term list * thm list * (int list list * thm list list))) * local_theory
+    ((string list * (binding -> binding) list) *
+    (term list * thm list * (int list list * thm list list))) * local_theory
 end;
 
 structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR =
@@ -509,6 +510,7 @@
 
     val (bs, mxs) = map_split (apfst fst) fixes;
     val fun_names = map Binding.name_of bs;
+    val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs;
     val eqns_data = map (dissect_eqn lthy0 fun_names) specs;
     val funs_data = eqns_data
       |> partition_eq (op = o apply2 #fun_name)
@@ -569,21 +571,23 @@
 
     val notes =
       (if n2m then
-         map2 (fn name => fn thm => (name, inductN, [thm], induct_attrs)) fun_names
-           (take actual_nn inducts)
+         @{map 3} (fn name => fn qualify => fn thm => (name, qualify, inductN, [thm], induct_attrs))
+         fun_names qualifys (take actual_nn inducts)
        else
          [])
-      |> map (fn (prefix, thmN, thms, attrs) =>
-        ((Binding.qualify true prefix (Binding.name thmN), attrs), [(thms, [])]));
+      |> map (fn (prefix, qualify, thmN, thms, attrs) =>
+        ((qualify (Binding.qualify true prefix (Binding.name thmN)), attrs), [(thms, [])]));
 
     val common_name = mk_common_name fun_names;
+    val common_qualify = fold_rev I qualifys;
 
     val common_notes =
       (if n2m then [(inductN, [common_induct], [])] else [])
       |> map (fn (thmN, thms, attrs) =>
-        ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
+        ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs),
+          [(thms, [])]));
   in
-    (((fun_names, defs),
+    (((fun_names, qualifys, defs),
       fn lthy => fn defs =>
         let
           val def_thms = map (snd o snd) defs;
@@ -606,14 +610,14 @@
     val nonexhaustives = replicate actual_nn nonexhaustive;
     val transfers = replicate actual_nn transfer;
 
-    val (((names, defs), prove), lthy') =
+    val (((names, qualifys, defs), prove), lthy') =
       prepare_primrec plugins nonexhaustives transfers fixes ts lthy;
   in
     lthy'
     |> fold_map Local_Theory.define defs
     |-> (fn defs => fn lthy =>
       let val ((jss, simpss), lthy) = prove lthy defs in
-        ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
+        (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
       end)
   end;
 
@@ -621,7 +625,8 @@
   primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
   handle OLD_PRIMREC () =>
     Old_Primrec.primrec_simple fixes ts lthy
-    |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single;
+    |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single
+    |>> apfst (map_split (rpair I));
 
 fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy =
   let
@@ -638,7 +643,7 @@
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
-      flat ooo @{map 3} (fn js => fn prefix => fn thms =>
+      flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
         let
           val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
@@ -647,14 +652,14 @@
                  [([thm], [])]))
               bs attrss thms;
         in
-          ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
+          ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes
         end);
   in
     lthy
     |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
-    |-> (fn (names, (ts, defs, (jss, simpss))) =>
+    |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
-      #> Local_Theory.notes (mk_notes jss names simpss)
+      #> Local_Theory.notes (mk_notes jss names qualifys simpss)
       #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>