src/Pure/Isar/named_target.ML
changeset 45353 68f3e073ee21
parent 45352 0b4038361a3a
child 45375 7fe19930dfc9
     1.1 --- a/src/Pure/Isar/named_target.ML	Sat Nov 05 22:01:19 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sat Nov 05 22:41:25 2011 +0100
     1.3 @@ -158,10 +158,12 @@
     1.4      val target_name =
     1.5        [Pretty.command (if is_class then "class" else "locale"),
     1.6          Pretty.str (" " ^ Locale.extern thy target)];
     1.7 -    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
     1.8 -      (#1 (Proof_Context.inferred_fixes ctxt));
     1.9 -    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.10 -      (Assumption.all_assms_of ctxt);
    1.11 +    val fixes =
    1.12 +      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.13 +        (#1 (Proof_Context.inferred_fixes ctxt));
    1.14 +    val assumes =
    1.15 +      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.16 +        (Assumption.all_assms_of ctxt);
    1.17      val elems =
    1.18        (if null fixes then [] else [Element.Fixes fixes]) @
    1.19        (if null assumes then [] else [Element.Assumes assumes]);