--- 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");
--- 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