--- a/src/Pure/Isar/args.ML Sat Apr 14 00:46:18 2007 +0200
+++ b/src/Pure/Isar/args.ML Sat Apr 14 00:46:20 2007 +0200
@@ -189,7 +189,7 @@
| Typ T => Typ (Morphism.typ phi T)
| Term t => Term (Morphism.term phi t)
| Fact ths => Fact (Morphism.fact phi ths)
- | Attribute att => Attribute (fn psi => att (phi $> psi))));
+ | Attribute att => Attribute (Morphism.transform phi att)));
fun maxidx_values (Src ((_, args), _)) = args |> fold
(fn (Arg (_, Value (SOME (Typ T)))) => Term.maxidx_typ T
--- a/src/Pure/Isar/attrib.ML Sat Apr 14 00:46:18 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Sat Apr 14 00:46:20 2007 +0200
@@ -265,7 +265,7 @@
fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
fun internal_att x =
- syntax (Scan.lift Args.internal_attribute >> (fn att => att Morphism.identity)) x;
+ syntax (Scan.lift Args.internal_attribute >> Morphism.form) x;
(* theory setup *)
--- 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