1.1 --- a/src/Pure/Isar/attrib.ML	Sat Nov 19 13:36:38 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Nov 19 14:31:43 2011 +0100
     1.3 @@ -219,11 +219,11 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** partial evaluation **)
     1.8 +(** partial evaluation -- observing rule/declaration/mixed attributes **)
     1.9  
    1.10  local
    1.11  
    1.12 -val strict_thm_eq = op = o pairself Thm.rep_thm;
    1.13 +val strict_eq_thm = op = o pairself Thm.rep_thm;
    1.14  
    1.15  fun apply_att src (context, th) =
    1.16    let
    1.17 @@ -246,7 +246,7 @@
    1.18            (case decls of
    1.19              [] => [(th, [src'])]
    1.20            | (th2, srcs2) :: rest =>
    1.21 -              if strict_thm_eq (th, th2)
    1.22 +              if strict_eq_thm (th, th2)
    1.23                then ((th2, src' :: srcs2) :: rest)
    1.24                else (th, [src']) :: (th2, srcs2) :: rest);
    1.25        in ((th, NONE), (decls', context')) end
    1.26 @@ -263,25 +263,27 @@
    1.27  in
    1.28  
    1.29  fun partial_evaluation ctxt facts =
    1.30 -  let
    1.31 -    val (facts', (decls, _)) =
    1.32 -      (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
    1.33 -        fold_map (fn ((b, more_atts), fact) => fn res =>
    1.34 -          let
    1.35 -            val (fact', res') =
    1.36 -              (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
    1.37 -                (ths, res1) |-> fold_map (fn th => fn res2 =>
    1.38 -                  let
    1.39 -                    val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
    1.40 -                    val th_atts' =
    1.41 -                      (case dyn' of
    1.42 -                        NONE => ([th'], [])
    1.43 -                      | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
    1.44 -                  in (th_atts', res3) end))
    1.45 -              |>> flat;
    1.46 -          in (((b, []), fact'), res') end);
    1.47 -    val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
    1.48 -  in decl_fact :: facts' end;
    1.49 +  (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
    1.50 +    fold_map (fn ((b, more_atts), fact) => fn context =>
    1.51 +      let
    1.52 +        val (fact', (decls, context')) =
    1.53 +          (fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 =>
    1.54 +            (ths, res1) |-> fold_map (fn th => fn res2 =>
    1.55 +              let
    1.56 +                val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
    1.57 +                val th_atts' =
    1.58 +                  (case dyn' of
    1.59 +                    NONE => (th', [])
    1.60 +                  | SOME (dyn_th', atts') => (dyn_th', rev atts'));
    1.61 +              in (th_atts', res3) end))
    1.62 +          |>> flat;
    1.63 +        val decls' = rev (map (apsnd rev) decls);
    1.64 +        val facts' =
    1.65 +          if eq_list (eq_fst strict_eq_thm) (decls', fact') then
    1.66 +            [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
    1.67 +          else [(empty_binding, decls'), ((b, []), fact')];
    1.68 +      in (facts', context') end)
    1.69 +  |> fst |> flat |> map (apsnd (map (apfst single)));
    1.70  
    1.71  end;
    1.72