--- a/src/Pure/meta_simplifier.ML Sat Apr 14 00:46:18 2007 +0200
+++ b/src/Pure/meta_simplifier.ML Sat Apr 14 00:46:20 2007 +0200
@@ -623,7 +623,7 @@
Simproc
{name = name,
lhss = map (Morphism.cterm phi) lhss,
- proc = fn psi => proc (phi $> psi),
+ proc = Morphism.transform phi proc,
id = (s, Morphism.fact phi ths)};
fun make_simproc {name, lhss, proc, identifier} =
@@ -656,7 +656,7 @@
(warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
fun prep_procs (Simproc {name, lhss, proc, id}) =
- lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc Morphism.identity, id = id});
+ lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
in