--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:37:53 2013 +0200
@@ -56,9 +56,9 @@
("{_} // _ // {_}" [0,55,0] 50)
ML_file "hoare_syntax.ML"
-parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
print_translation
- {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
+ {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))] *}
(*** The proof rules ***)