src/HOL/Tools/BNF/bnf_def.ML

--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -829,7 +829,7 @@
 
     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 =