src/Pure/Isar/attrib.ML
changeset 55740 11dd48f84441
parent 55140 7eb0c04e4c40
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Feb 25 10:50:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Feb 25 11:36:04 2014 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4        let
     1.5          val atts = map (attribute_generic context) srcs;
     1.6          val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
     1.7 -      in (context', pick "" [th']) end)
     1.8 +      in (context', pick ("", Position.none) [th']) end)
     1.9      ||
    1.10      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.11        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    1.12 @@ -244,7 +244,7 @@
    1.13          val atts = map (attribute_generic context) srcs;
    1.14          val (ths', context') =
    1.15            fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    1.16 -      in (context', pick name ths') end)
    1.17 +      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
    1.18    end);
    1.19  
    1.20  in