# HG changeset patch
# User wenzelm
# Date 1220386821 -7200
# Node ID 5f340fb49b9094f0f7444e08ba60bf6519217c76
# Parent  d81a4ed6b538d3b3e27c37329df8e5469dd4ae12
tuned;

diff -r d81a4ed6b538 -r 5f340fb49b90 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 22:20:20 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 22:20:21 2008 +0200
@@ -48,10 +48,10 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
-    val fixes = map (fn (x, T) =>
-      (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
-    val assumes = map (fn A =>
-      (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
+    val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
+      (#1 (ProofContext.inferred_fixes ctxt));
+    val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
+      (Assumption.assms_of ctxt);
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);