# HG changeset patch
# User wenzelm
# Date 1007427614 -3600
# Node ID 92c48cc45e78d635725b72092cb62b715050d87a
# Parent  54aef8e41437907f0a3d297d5fdbc9eae2e07263
renamed RuleContext to ContextRules;

diff -r 54aef8e41437 -r 92c48cc45e78 src/FOL/IFOL.thy
--- 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));
 *}