| changeset 16121 | a80aa66d2271 |
| parent 16019 | 0e1405402d53 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/HOL.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/HOL.thy Tue May 31 11:53:12 2005 +0200 @@ -899,8 +899,8 @@ use "cladata.ML" setup hypsubst_setup -ML_setup {* - Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); +setup {* + [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)] *} setup Classical.setup