Morphism.fact;
authorwenzelm
Tue, 02 Jan 2007 22:43:05 +0100
changeset 21976 1f608af40542
parent 21975 1152dc45d591
child 21977 7f7177a95189
Morphism.fact;
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