# HG changeset patch
# User wenzelm
# Date 1427573102 -3600
# Node ID 2333045edb78c786991dc277322d7ba80b9fcd82
# Parent  057b1018d5893b0cf50e0a5e488c023b7edb1c9b# Parent  96008563bfee540dfe17ec2d70dfc0f4bf61d493
merged

diff -r 96008563bfee -r 2333045edb78 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sat Mar 28 20:22:10 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sat Mar 28 21:05:02 2015 +0100
@@ -865,25 +865,25 @@
 \item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.case_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 This property is missing for @{typ "'a list"} because there is no common
 selector to all constructors. \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.ctr_transfer(1)[no_vars]} \\
 @{thm list.ctr_transfer(2)[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.disc_transfer(1)[no_vars]} \\
 @{thm list.disc_transfer(2)[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
@@ -958,7 +958,7 @@
 \item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.set_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
 @{thm list.map_cong0[no_vars]}
@@ -981,7 +981,7 @@
 \item[@{text "t."}\hthm{map_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.map_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
 @{thm list.rel_compp[no_vars]} \\
@@ -1012,7 +1012,7 @@
 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rel_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -1053,7 +1053,7 @@
 \item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rec_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -1928,7 +1928,7 @@
 \item[@{text "t."}\hthm{corec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm llist.corec_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -3066,7 +3066,8 @@
 the \hthm{transfer} plugin generates a predicator @{text "t.pred_t"} and
 properties that guide the Transfer tool.
 
-The plugin derives the following properties:
+For types with no dead type arguments (and at least one live type argument), the
+plugin derives the following properties:
 
 \begin{indentblock}
 \begin{description}
diff -r 96008563bfee -r 2333045edb78 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 28 21:05:02 2015 +0100
@@ -791,7 +791,10 @@
 
     val repTA = mk_T_of_bnf Ds As bnf;
     val T_bind = qualify b;
-    val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
+    val all_TA_params_in_order = Term.add_tfreesT repTA As';
+    val TA_params =
+      (if has_live_phantoms then all_TA_params_in_order
+       else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order);
     val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
       maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
         (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
@@ -906,7 +909,9 @@
     val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
       |> map (fn (b, def) => ((b, []), [([def], [])]))
 
-    val (noted, lthy'') = lthy' |> Local_Theory.notes notes
+    val (noted, lthy'') = lthy'
+      |> Local_Theory.notes notes
+      ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'')
   in
     ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
   end;
diff -r 96008563bfee -r 2333045edb78 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sat Mar 28 21:05:02 2015 +0100
@@ -1609,7 +1609,8 @@
           [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
             Pretty.quote (Syntax.pretty_term ctxt bd)]]);
   in
-    Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
+    Pretty.big_list "Registered bounded natural functors:"
+      (map pretty_bnf (sort_wrt fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
     |> Pretty.writeln
   end;
 
diff -r 96008563bfee -r 2333045edb78 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Sat Mar 28 21:05:02 2015 +0100
@@ -93,7 +93,7 @@
   in
     [((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]    
   end
-  handle ERROR _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
+  handle NO_PRED_DATA _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
 
 (* relator_mono  *)
 
diff -r 96008563bfee -r 2333045edb78 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Sat Mar 28 21:05:02 2015 +0100
@@ -6,6 +6,8 @@
 
 signature TRANSFER_BNF =
 sig
+  exception NO_PRED_DATA of unit
+
   val transfer_plugin: string
   val base_name_of_bnf: BNF_Def.bnf -> binding
   val type_name_of_bnf: BNF_Def.bnf -> string
@@ -21,6 +23,8 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 
+exception NO_PRED_DATA of unit
+
 val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
 
 (* util functions *)
@@ -318,9 +322,9 @@
 (* simplification rules for the predicator *)
 
 fun lookup_defined_pred_data lthy name =
-  case (Transfer.lookup_pred_data lthy name) of
+  case Transfer.lookup_pred_data lthy name of
     SOME data => data
-    | NONE => (error "lookup_pred_data: something went utterly wrong")
+  | NONE => raise NO_PRED_DATA ()
 
 fun lives_of_fp (fp_sugar: fp_sugar) =
   let
@@ -377,6 +381,7 @@
     |> Variable.export lthy old_lthy
     |> map Drule.zero_var_indexes
   end
+  handle NO_PRED_DATA () => []
 
 
 (* fp_sugar interpretation *)