Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 28 Dec 2015 16:13:15 +0100
changeset 61948 52972bed8e2e
parent 61947 8d996ee7e986
child 61949 d9acd750c1f6
tuned;
src/HOL/Tools/inductive.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle