src/HOL/BNF/Tools/bnf_def.ML

   let
     val fact_policy = mk_fact_policy no_defs_lthy;
     val bnf_b = qualify raw_bnf_b;
     val live = length raw_sets;
 
-    val bnf_rhs_T = prep_typ no_defs_lthy raw_bnf_T;
+    val T_rhs = prep_typ no_defs_lthy raw_bnf_T;
     val map_rhs = prep_term no_defs_lthy raw_map;
     val set_rhss = map (prep_term no_defs_lthy) raw_sets;
     val bd_rhs = prep_term no_defs_lthy raw_bd;
 
     fun err T =
       error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
         " as unnamed BNF");
 
     val (bnf_b, key) =
       if Binding.eq_name (bnf_b, Binding.empty) then
-        (case bnf_rhs_T of
+        (case T_rhs of
           Type (C, Ts) => if forall (can dest_TFree) Ts
-            then (Binding.qualified_name C, C) else err bnf_rhs_T
+            then (Binding.qualified_name C, C) else err T_rhs
         | T => err T)
       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
 
     val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
 

       handle TYPE _ => error "Bad map function";
 
     val CA_params = map TVar (Term.add_tvarsT CA []);
 
     val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms);
-    val bnf_T = Morphism.typ phi bnf_rhs_T;
+    val bnf_T = Morphism.typ phi T_rhs;
     val bnf_bd =
       Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
 
     (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
     val deads = (case Ds_opt of