# HG changeset patch
# User blanchet
# Date 1377781362 -7200
# Node ID d4784d3d3a54bd7aa1fbf970df436eca6cc2fce5
# Parent  23927b18dce2b4616faae4307a5d01ab2180a61e
rationalized bindings

diff -r 23927b18dce2 -r d4784d3d3a54 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 13:51:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 15:02:42 2013 +0200
@@ -584,10 +584,9 @@
 
     val common_name = mk_common_name (map Binding.name_of bs);
 
-    fun raw_qualify b =
-      let val s = Binding.name_of b in
-        Binding.qualify false s o Binding.qualify true (rawN ^ s)
-      end;
+    fun raw_qualify base_b =
+      Binding.prefix_name rawN
+      #> fold_rev (fn (s, mand) => Binding.qualify mand s) (#2 (Binding.dest base_b));
 
     val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
@@ -608,10 +607,8 @@
 
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
-    fun pre_binding b = Binding.qualify false (Binding.name_of b) (Binding.prefix_name preN b);
-
     val ((pre_bnfs, deadss), lthy'') =
-      fold_map3 (seal_bnf unfold_set') (map pre_binding bs) Dss bnfs' lthy'
+      fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
       |>> split_list;
 
     val timer = time (timer "Normalization & sealing of BNFs");
diff -r 23927b18dce2 -r d4784d3d3a54 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Aug 29 13:51:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Aug 29 15:02:42 2013 +0200
@@ -323,7 +323,7 @@
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
 
-(* The standard binding stands for a name generated following the canonical convention (e.g.
+(* The standard binding stands for a name generated following the canonical convention (e.g.,
    "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
    depending on the context. *)
 val standard_binding = @{binding _};
@@ -334,11 +334,13 @@
 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
 
 (*TODO: is this really different from Typedef.add_typedef_global?*)
-fun typedef typ set opt_morphs tac lthy =
+fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   let
+    (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
+    val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Typedef.add_typedef typ set opt_morphs tac
+      |> Typedef.add_typedef (b', Ts, mx) set opt_morphs tac
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in