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.
less verbose inductive invocation
authorkrauss
Fri, 30 Oct 2009 01:32:06 +0100
changeset 33350 b2b78c5ef771
parent 33349 634376549164
child 33351 37ec56ac3fd4
less verbose inductive invocation
src/HOL/Tools/Function/function_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/function_core.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -458,8 +458,8 @@
       lthy
       |> LocalTheory.conceal
       |> Inductive.add_inductive_i
-          {quiet_mode = false,
-            verbose = ! Toplevel.debug,
+          {quiet_mode = true,
+            verbose = ! trace,
             kind = Thm.internalK,
             alt_name = Binding.empty,
             coind = false,
isabelle