# HG changeset patch
# User blanchet
# Date 1425977357 -3600
# Node ID fb544855e3b14bbf66d2d63bbecdee0f153c90fa
# Parent  c875b71086a3d5f1a6b4420878bb3b9d1ec85ca3
split into subgoals

diff -r c875b71086a3 -r fb544855e3b1 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 10 09:49:16 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 10 09:49:17 2015 +0100
@@ -1568,8 +1568,11 @@
       | SOME tac => (mk_triv_wit_thms tac, []));
   in
     Proof.unfolding ([[(defs, [])]])
-      (Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
-        (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
+      (lthy
+       |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
+         (map (single o rpair []) goals @ nontriv_wit_goals)
+       |> Proof.refine (Method.primitive_text (K I))
+       |> Seq.hd)
   end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
     NONE Binding.empty Binding.empty [] raw_csts;
 
@@ -1577,7 +1580,7 @@
   let
     fun pretty_set sets i = Pretty.block
       [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
-          Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
+        Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
 
     fun pretty_bnf (key, BNF {T, map, sets, bd, live, lives, dead, deads, ...}) =
       Pretty.big_list