src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

       user_eqn = user_eqn
     }, matchedsss')
   end;
 
 fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
-    ctr_rhs_opt code_rhs_opt eqn' of_spec_opt eqn =
+    ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn =
   let
     val (lhs, rhs) = HOLogic.dest_eq eqn
       handle TERM _ =>
         primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
     val sel = head_of lhs;

     val {ctr, ...} =
       (case of_spec_opt of
         SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
       | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
           handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
-    val user_eqn = drop_All eqn';
+    val user_eqn = drop_All eqn0;
   in
     Sel {
       fun_name = fun_name,
       fun_T = fun_T,
       fun_args = fun_args,

       user_eqn = user_eqn
     }
   end;
 
 fun dissect_coeqn_ctr fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
-    eqn_pos eqn' code_rhs_opt prems concl matchedsss =
+    eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
   let
     val (lhs, rhs) = HOLogic.dest_eq concl;
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
     val (ctr, ctr_args) = strip_comb (unfold_let rhs);

  space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) prems));
 *)
 
     val eqns_data_sel =
       map (dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos
-        (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn' (SOME ctr)) sel_concls;
+        (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
   in
     (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss')
   end;
 
-fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn' concl matchedsss =
+fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
   let
     val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []);
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
 

         |> curry list_comb ctr
         |> curry HOLogic.mk_eq lhs);
 
     val sequentials = replicate (length fun_names) false;
   in
-    fold_map2 (dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn'
+    fold_map2 (dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
         (SOME (abstract (List.rev fun_args) rhs)))
       ctr_premss ctr_concls matchedsss
   end;
 
 fun dissect_coeqn lthy has_call fun_names sequentials
-    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn') of_spec_opt matchedsss =
+    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
   let
-    val eqn = drop_All eqn'
-      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn';
+    val eqn = drop_All eqn0
+      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
     val (prems, concl) = Logic.strip_horn eqn
       |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
 
     val head = concl
       |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))

     val discs = maps (map #disc) basic_ctr_specss;
     val sels = maps (maps #sels) basic_ctr_specss;
     val ctrs = maps (map #ctr) basic_ctr_specss;
   in
     if member (op =) discs head orelse
-      is_some rhs_opt andalso
-        member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
-      dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl matchedsss
+        is_some rhs_opt andalso
+          member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
+      dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
+        matchedsss
       |>> single
     else if member (op =) sels head then
-      ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn' of_spec_opt concl],
+      ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
        matchedsss)
-    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
-      member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
-      dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn' NONE prems concl matchedsss
-    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
-      null prems then
-      dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn' concl matchedsss
-      |>> flat
+    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
+      if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
+        dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
+          (if null prems then SOME eqn0 else NONE) prems concl matchedsss
+      else if null prems then
+        dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
+        |>> flat
+      else
+        primcorec_error_eqn "malformed constructor or code view equation" eqn
     else
       primcorec_error_eqn "malformed function equation" eqn
   end;
 
 fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)

 val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
  space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
 *)
 
     val excludess'' = map2 (fn sequential => map (fn (idx, goal) =>
-        (idx, (Option.map (Goal.prove lthy [] [] goal #> Thm.close_derivation)
+        (idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac sequential idx), goal))))
       sequentials excludess';
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
     val (goal_idxss, goalss') = excludess''
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))

         disc_eqnss;
     val de_facto_exhaustives =
       map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;
 
     fun map_prove_with_tac tac =
-      map (fn goal => Goal.prove lthy [] [] goal tac |> Thm.close_derivation);
+      map (fn goal => Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation);
 
     val nchotomy_goalss =
       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []

           |> list_all_fun_args ps
           |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
               | [nchotomy_thm] => fn [goal] =>
                 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
                    (length disc_eqns) nchotomy_thm
-                 |> K |> Goal.prove lthy [] [] goal
+                 |> K |> Goal.prove_sorry lthy [] [] goal
                  |> Thm.close_derivation])
             disc_eqnss nchotomy_thmss;
         val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
 
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);

             in
               if prems = [@{term False}] then
                 []
               else
                 mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair (#disc (nth ctr_specs ctr_no))
                 |> pair eqn_pos
                 |> single
             end;

               |> curry Logic.list_all (map dest_Free fun_args);
             val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
           in
             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
               nested_map_comps sel_corec k m excludesss
-            |> K |> Goal.prove lthy [] [] goal
+            |> K |> Goal.prove_sorry lthy [] [] goal
             |> Thm.close_derivation
             |> pair sel
             |> pair eqn_pos
           end;
 

           if not (exists (curry (op =) ctr o #ctr) disc_eqns)
               andalso not (exists (curry (op =) ctr o #ctr) sel_eqns)
             orelse
               filter (curry (op =) ctr o #ctr) sel_eqns
               |> fst o finds ((op =) o apsnd #sel) sels
-              |> exists (null o snd)
-          then [] else
+              |> exists (null o snd) then
+            []
+          else
             let
               val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) =
                 (find_first (curry (op =) ctr o #ctr) disc_eqns,
                  find_first (curry (op =) ctr o #ctr) sel_eqns)
                 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x,

               val disc_thm_opt = AList.lookup (op =) disc_alist disc;
               val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
             in
               if prems = [@{term False}] then [] else
                 mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm_opt sel_thms
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair ctr
                 |> pair eqn_pos
                 |> single
             end;

                       case_thms_of_term lthy bound_Ts raw_rhs;
 
                     val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
                         sel_splits sel_split_asms ms ctr_thms
                         (if exhaustive_code then try the_single nchotomys else NONE)
-                      |> K |> Goal.prove lthy [] [] raw_goal
+                      |> K |> Goal.prove_sorry lthy [] [] raw_goal
                       |> Thm.close_derivation;
                   in
                     mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
-                    |> K |> Goal.prove lthy [] [] goal
+                    |> K |> Goal.prove_sorry lthy [] [] goal
                     |> Thm.close_derivation
                     |> single
                   end)
               end)
           end;

               if prems = [@{term False}] then
                 []
               else
                 mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) fun_args)
                   (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair eqn_pos
                 |> single
             end;