# HG changeset patch
# User wenzelm
# Date 1451315595 -3600
# Node ID 52972bed8e2e92d88c9f128c997cdb5b8e5f01a0
# Parent  8d996ee7e986e570ecef46bf9dc49c1a6262d91b
tuned;

diff -r 8d996ee7e986 -r 52972bed8e2e src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Dec 28 15:11:03 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Dec 28 16:13:15 2015 +0100
@@ -839,6 +839,8 @@
 
     (* add definition of recursive predicates to theory *)
 
+    val is_auxiliary = length cs > 1;
+
     val rec_binding =
       if Binding.is_empty alt_name then
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
@@ -846,7 +848,6 @@
     val rec_name = Binding.name_of rec_binding;
 
     val inductive_defs = Config.get lthy inductive_defs;
-    val is_auxiliary = length cs >= 2;
 
     val ((rec_const, (_, fp_def)), lthy') = lthy
       |> is_auxiliary ? Proof_Context.concealed