1# HG changeset patch
2# Parent 8f4a332500e41bb67efc3e141608829473606a72
3#
4# Copyright 2014, NICTA
5#
6# This software may be distributed and modified according to the terms of
7# the BSD 2-Clause license. Note that NO WARRANTY is provided.
8# See "LICENSE_BSD2.txt" for details.
9#
10# @TAG(NICTA_BSD)
11#
12
13diff --git a/src/HOL/ROOT b/src/HOL/ROOT
14--- a/src/HOL/ROOT
15+++ b/src/HOL/ROOT
16@@ -8,6 +8,8 @@
17   global_theories
18     Main
19     Complex_Main
20+  theories
21+    "$ISABELLE_PROOFCOUNT_HOME/ProofCount"
22   files
23     "Tools/Quickcheck/Narrowing_Engine.hs"
24     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
25diff --git a/src/Pure/Isar/outer_syntax.ML b/src/Pure/Isar/outer_syntax.ML
26--- a/src/Pure/Isar/outer_syntax.ML
27+++ b/src/Pure/Isar/outer_syntax.ML
28@@ -161,7 +161,7 @@
29   in
30     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
31      (if not (Symtab.defined commands name) then ()
32-      else if ! batch_mode then
33+      else if false then
34         error ("Attempt to redefine outer syntax command " ^ command_name)
35       else
36         warning ("Redefining outer syntax command " ^ command_name ^
37