# HG changeset patch
# User wenzelm
# Date 1167774185 -3600
# Node ID 1f608af405426b7780dba31e58d0b5549ab76e9f
# Parent  1152dc45d59105d89fc1f1e98dc0050c054771c0
Morphism.fact;

diff -r 1152dc45d591 -r 1f608af40542 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Jan 02 22:43:04 2007 +0100
+++ b/src/Pure/Isar/args.ML	Tue Jan 02 22:43:05 2007 +0100
@@ -188,7 +188,7 @@
   (fn Text s => Text s
     | Typ T => Typ (Morphism.typ phi T)
     | Term t => Term (Morphism.term phi t)
-    | Fact ths => Fact (map (Morphism.thm phi) ths)
+    | Fact ths => Fact (Morphism.fact phi ths)
     | Attribute att => Attribute (fn psi => att (phi $> psi))));
 
 fun maxidx_values (Src ((_, args), _)) = args |> fold