partial evaluation in invisible context;
authorwenzelm
Thu Nov 17 21:31:29 2011 +0100 (2011-11-17)
changeset 455378e3e004f1c31
parent 45536 5b0b1dc2e40f
child 45538 1fffa81b9b83
partial evaluation in invisible context;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Nov 17 19:01:05 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Nov 17 21:31:29 2011 +0100
     1.3 @@ -262,20 +262,21 @@
     1.4  fun partial_evaluation ctxt facts =
     1.5    let
     1.6      val (facts', (decls, _)) =
     1.7 -      (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
     1.8 -        let
     1.9 -          val (fact', res') =
    1.10 -            (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
    1.11 -              (ths, res1) |-> fold_map (fn th => fn res2 =>
    1.12 -                let
    1.13 -                  val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
    1.14 -                  val th_atts' =
    1.15 -                    (case dyn' of
    1.16 -                      NONE => ([th'], [])
    1.17 -                    | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
    1.18 -                in (th_atts', res3) end))
    1.19 -            |>> flat;
    1.20 -        in (((b, []), fact'), res') end);
    1.21 +      (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
    1.22 +        fold_map (fn ((b, more_atts), fact) => fn res =>
    1.23 +          let
    1.24 +            val (fact', res') =
    1.25 +              (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
    1.26 +                (ths, res1) |-> fold_map (fn th => fn res2 =>
    1.27 +                  let
    1.28 +                    val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
    1.29 +                    val th_atts' =
    1.30 +                      (case dyn' of
    1.31 +                        NONE => ([th'], [])
    1.32 +                      | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
    1.33 +                  in (th_atts', res3) end))
    1.34 +              |>> flat;
    1.35 +          in (((b, []), fact'), res') end);
    1.36      val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
    1.37    in decl_fact :: facts' end;
    1.38