--- a/src/Pure/Isar/theory_target.ML Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML Tue Sep 02 16:55:33 2008 +0200
@@ -51,7 +51,7 @@
val fixes = map (fn (x, T) =>
(Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
val assumes = map (fn A =>
- ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
+ (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);