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