# HG changeset patch
# User wenzelm
# Date 1608811431 -3600
# Node ID 7ea253f9360609926c2f364daf460b7d7fb2382f
# Parent  a562a0f656e8adf38129b54b0e4fc720b46b55b1
more robust: clarified error when merging Hoare_Logic + Hoare_Logic_Abort;

diff -r a562a0f656e8 -r 7ea253f93606 src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Thu Dec 24 12:58:25 2020 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML	Thu Dec 24 13:03:51 2020 +0100
@@ -206,11 +206,14 @@
 
 (** setup **)
 
+val _ =
+  Theory.setup
+   (Sign.parse_translation
+    [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
+     (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);
+
 fun setup consts =
   Data.put (SOME consts) #>
-  Sign.parse_translation
-   [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
-    (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)] #>
   Sign.print_translation
    [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
     (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];