1.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 16 20:56:21 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 16 21:16:36 2011 +0100
     1.3 @@ -219,25 +219,30 @@
     1.4  (** partial evaluation **)
     1.5  
     1.6  local
     1.7 -(* FIXME assignable, closure (!?) *)
     1.8 +
     1.9 +val strict_thm_eq = op = o pairself Thm.rep_thm;
    1.10  
    1.11  fun apply_att src (context, th) =
    1.12 -  attribute_i (Context.theory_of context) src (context, th);
    1.13 +  let
    1.14 +    val src1 = Args.assignable src;
    1.15 +    val result = attribute_i (Context.theory_of context) src1 (context, th);
    1.16 +    val src2 = Args.closure src1;
    1.17 +  in (src2, result) end;
    1.18  
    1.19  fun eval src (th, (decls, context)) =
    1.20    (case apply_att src (context, th) of
    1.21 -    (NONE, SOME th') => (th', (decls, context))
    1.22 -  | (opt_context', opt_th') =>
    1.23 +    (_, (NONE, SOME th')) => (th', (decls, context))
    1.24 +  | (src', (opt_context', opt_th')) =>
    1.25        let
    1.26          val context' = the_default context opt_context';
    1.27          val th' = the_default th opt_th';
    1.28          val decls' =
    1.29            (case decls of
    1.30 -            [] => [(th, [src])]
    1.31 +            [] => [(th, [src'])]
    1.32            | (th2, srcs2) :: rest =>
    1.33 -              if op = (pairself Thm.rep_thm (th, th2))  (* FIXME derivation!? *)
    1.34 -              then ((th2, src :: srcs2) :: rest)
    1.35 -              else (th, [src]) :: (th2, srcs2) :: rest);
    1.36 +              if strict_thm_eq (th, th2)
    1.37 +              then ((th2, src' :: srcs2) :: rest)
    1.38 +              else (th, [src']) :: (th2, srcs2) :: rest);
    1.39        in (th', (decls', context')) end);
    1.40  
    1.41  in
    1.42 @@ -247,10 +252,11 @@
    1.43      val (facts', (decls, _)) =
    1.44        (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
    1.45          let
    1.46 -          val (thss', res') =
    1.47 +          val (ths', res') =
    1.48              (fact, res) |-> fold_map (fn (ths, atts) =>
    1.49 -              fold_map (curry (fold eval (atts @ more_atts))) ths);
    1.50 -        in (((b, []), [(flat thss', [])]), res') end);
    1.51 +              fold_map (curry (fold eval (atts @ more_atts))) ths)
    1.52 +            |>> flat;
    1.53 +        in (((b, []), [(ths', [])]), res') end);
    1.54      val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
    1.55    in decl_fact :: facts' end;
    1.56