1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 22:20:20 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 22:20:21 2008 +0200
     1.3 @@ -48,10 +48,10 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
     1.7 -    val fixes = map (fn (x, T) =>
     1.8 -      (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     1.9 -    val assumes = map (fn A =>
    1.10 -      (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
    1.11 +    val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
    1.12 +      (#1 (ProofContext.inferred_fixes ctxt));
    1.13 +    val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
    1.14 +      (Assumption.assms_of ctxt);
    1.15      val elems =
    1.16        (if null fixes then [] else [Element.Fixes fixes]) @
    1.17        (if null assumes then [] else [Element.Assumes assumes]);