--- a/src/Provers/eqsubst.ML Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Provers/eqsubst.ML Fri Feb 10 02:22:16 2006 +0100
@@ -331,7 +331,7 @@
should be done to an assumption, false = apply to the conclusion of
the goal) as well as the theorems to use *)
fun subst_meth src =
- Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src
+ Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
#> (fn (ctxt, ((asmflag, occL), inthms)) =>
(if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);