src/HOL/Codatatype/Tools/bnf_def.ML

 
     fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy3 QTs CA' CB' bnf_pred;
 
     val pred = mk_bnf_pred QTs CA' CB';
 
-    val goal_map_id =
+    val map_id_goal =
       let
         val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
       in
         HOLogic.mk_Trueprop
           (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA'))
       end;
 
-    val goal_map_comp =
+    val map_comp_goal =
       let
         val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
         val comp_bnf_map_app = HOLogic.mk_comp
           (Term.list_comb (bnf_map_BsCs, gs),
            Term.list_comb (bnf_map_AsBs, fs));
       in
         fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
       end;
 
-    val goal_map_cong =
+    val map_cong_goal =
       let
         fun mk_prem z set f f_copy =
           Logic.all z (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
             mk_Trueprop_eq (f $ z, f_copy $ z)));

       in
         fold_rev Logic.all (x :: fs @ fs_copy)
           (Logic.list_implies (prems, HOLogic.mk_Trueprop eq))
       end;
 
-    val goal_set_naturals =
+    val set_naturals_goal =
       let
         fun mk_goal setA setB f =
           let
             val set_comp_map =
               HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));

           end;
       in
         map3 mk_goal bnf_sets_As bnf_sets_Bs fs
       end;
 
-    val goal_card_order_bd = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
-
-    val goal_cinfinite_bd = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
-
-    val goal_set_bds =
+    val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
+
+    val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
+
+    val set_bds_goal =
       let
         fun mk_goal set =
           Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As));
       in
         map mk_goal bnf_sets_As
       end;
 
-    val goal_in_bd =
+    val in_bd_goal =
       let
         val bd = mk_cexp
           (if live = 0 then ctwo
             else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
           bnf_bd_As;
       in
         fold_rev Logic.all As
           (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd))
       end;
 
-    val goal_map_wpull =
+    val map_wpull_goal =
       let
         val prems = map HOLogic.mk_Trueprop
           (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s);
         val CX = mk_bnf_T domTs CA;
         val CB1 = mk_bnf_T B1Ts CA;

       in
         fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s)
           (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
       end;
 
-    val goal_rel_O_Gr =
+    val rel_O_Gr_goal =
       let
         val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
         val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
         val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
         (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
         val rhs = mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2);
       in
         fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs))
       end;
 
-    val goals = zip_goals goal_map_id goal_map_comp goal_map_cong goal_set_naturals
-      goal_card_order_bd goal_cinfinite_bd goal_set_bds goal_in_bd goal_map_wpull goal_rel_O_Gr;
+    val goals = zip_goals map_id_goal map_comp_goal map_cong_goal set_naturals_goal
+      card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
 
     fun mk_wit_goals (I, wit) =
       let
         val xs = map (nth bs) I;
         fun wit_goal i =

         val collect_set_natural = mk_lazy mk_collect_set_natural;
 
         fun mk_in_mono () =
           let
             val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_subset) As As_copy;
-            val goal_in_mono =
+            val in_mono_goal =
               fold_rev Logic.all (As @ As_copy)
                 (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
                   (mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
           in
-            Skip_Proof.prove lthy [] [] goal_in_mono (K (mk_in_mono_tac live))
+            Skip_Proof.prove lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
             |> Thm.close_derivation
           end;
 
         val in_mono = mk_lazy mk_in_mono;
 
         fun mk_in_cong () =
           let
             val prems_cong = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) As As_copy;
-            val goal_in_cong =
+            val in_cong_goal =
               fold_rev Logic.all (As @ As_copy)
                 (Logic.list_implies (prems_cong, HOLogic.mk_Trueprop
                   (HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))));
           in
-            Skip_Proof.prove lthy [] [] goal_in_cong (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+            Skip_Proof.prove lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
             |> Thm.close_derivation
           end;
 
         val in_cong = mk_lazy mk_in_cong;