src/HOL/Tools/BNF/bnf_def.ML

 
     val Calpha_params = map TVar (Term.add_tvarsT Calpha []);
 
     val bnf_T = Morphism.typ phi T_rhs;
     val bad_args = Term.add_tfreesT bnf_T [];
-    val _ = if null bad_args then () else error ("Locally fixed type arguments " ^
+    val _ = null bad_args orelse error ("Locally fixed type arguments " ^
       commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
 
     val bnf_sets =
       map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms);
     val bnf_bd =