# HG changeset patch
# User wenzelm
# Date 959776169 -7200
# Node ID 20e132267a83ff9a4b6f432daa34212af7740b5f
# Parent  963b7eb1b57b7829b3f4571c6593a03282ce8ae5
transfer now automatic;

diff -r 963b7eb1b57b -r 20e132267a83 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed May 31 14:27:12 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed May 31 14:29:29 2000 +0200
@@ -178,12 +178,8 @@
 (* print theorems / types / terms / props *)
 
 fun print_thms (ms, args) = Toplevel.keep (fn state =>
-  let
-    val st = Toplevel.node_case Proof.init_state Proof.enter_forward state;
-    val transfer = Thm.transfer (Toplevel.theory_of state);
-  in
-    with_modes ms (fn () =>
-      Pretty.writeln (Proof.pretty_thms (map transfer (IsarThy.get_thmss args st))))
+  let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state in
+    with_modes ms (fn () => Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st)))
   end);
 
 fun print_type (ms, s) = Toplevel.keep (fn state =>