| changeset 12352 | 92c48cc45e78 |
| parent 12349 | 94e812f9683e |
| child 12368 | 2af9ad81ea56 |
--- a/src/FOL/IFOL.thy Tue Dec 04 01:59:49 2001 +0100 +++ b/src/FOL/IFOL.thy Tue Dec 04 02:00:14 2001 +0100 @@ -152,7 +152,7 @@ and [Pure.intro] = exI disjI2 disjI1 ML_setup {* - Context.>> (RuleContext.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); + Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); *}