tuned interface

--- a/src/HOL/BNF_Composition.thy	Wed Mar 30 23:47:12 2016 +0200
+++ b/src/HOL/BNF_Composition.thy	Thu Mar 31 08:38:50 2016 +0200
@@ -81,9 +81,6 @@
 lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
   by blast
 
-lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
-by auto
-
 lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
   unfolding Grp_def fun_eq_iff relcompp.simps by auto
 

--- a/src/HOL/Tools/BNF/bnf_lift.ML	Wed Mar 30 23:47:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Thu Mar 31 08:38:50 2016 +0200
@@ -20,8 +20,8 @@
       string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) ->
       local_theory -> local_theory
   val lift_bnf:
-    (((lift_bnf_option list * (binding option * (string * sort option)) list) *
-      string) * thm option) * (binding * binding * binding) ->
+    ((((lift_bnf_option list * (binding option * (string * sort option)) list) *
+      string) * term list option) * thm option) * (binding * binding * binding) ->
       ({context: Proof.context, prems: thm list} -> tactic) list ->
       local_theory -> local_theory
   val lift_bnf_cmd:
@@ -378,7 +378,7 @@
   (fn (goals, after_qed, _, lthy) =>
     lthy
     |> after_qed (map2 (single oo Goal.prove lthy [] []) goals (tacs (length goals)))) oo
-  prepare_common prepare_name prepare_typ prepare_sort prepare_thm o apfst (apfst (rpair NONE));
+  prepare_common prepare_name prepare_typ prepare_sort prepare_thm;
 
 in
 
@@ -387,14 +387,17 @@
     (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
     Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms);
 
-fun lift_bnf args tacs = prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
+fun lift_bnf args tacs =
+  prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
 
 val copy_bnf =
-  prepare_solve (K I) (K I) (K I) (K I)
+  apfst (apfst (rpair NONE))
+  #> prepare_solve (K I) (K I) (K I) (K I)
     (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1));
 
 val copy_bnf_cmd =
-  prepare_solve
+  apfst (apfst (rpair NONE))
+  #> prepare_solve
     (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
     Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms)
     (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1));