src/Pure/Isar/theory_target.ML
changeset 28084 a05ca48ef263
parent 28083 103d9282a946
child 28094 5f340fb49b90
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 14:10:45 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 16:55:33 2008 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4      val fixes = map (fn (x, T) =>
     1.5        (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     1.6      val assumes = map (fn A =>
     1.7 -      ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
     1.8 +      (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
     1.9      val elems =
    1.10        (if null fixes then [] else [Element.Fixes fixes]) @
    1.11        (if null assumes then [] else [Element.Assumes assumes]);