--- a/src/HOL/HOL.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/HOL.thy Thu Jan 19 21:22:08 2006 +0100
@@ -911,9 +911,7 @@
use "cladata.ML"
setup hypsubst_setup
-setup {*
- [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)]
-*}
+setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
setup Classical.setup
setup clasetup
@@ -1233,7 +1231,7 @@
in
-val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
+val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen;
end;
*}