# HG changeset patch
# User wenzelm
# Date 1321561889 -3600
# Node ID 8e3e004f1c318f7e4cc58f7bb2f8f694e58dc6f7
# Parent  5b0b1dc2e40f30f99d21adf06fed1a54d5837a6c
partial evaluation in invisible context;

diff -r 5b0b1dc2e40f -r 8e3e004f1c31 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Nov 17 19:01:05 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Nov 17 21:31:29 2011 +0100
@@ -262,20 +262,21 @@
 fun partial_evaluation ctxt facts =
   let
     val (facts', (decls, _)) =
-      (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
-        let
-          val (fact', res') =
-            (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
-              (ths, res1) |-> fold_map (fn th => fn res2 =>
-                let
-                  val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
-                  val th_atts' =
-                    (case dyn' of
-                      NONE => ([th'], [])
-                    | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
-                in (th_atts', res3) end))
-            |>> flat;
-        in (((b, []), fact'), res') end);
+      (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
+        fold_map (fn ((b, more_atts), fact) => fn res =>
+          let
+            val (fact', res') =
+              (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
+                (ths, res1) |-> fold_map (fn th => fn res2 =>
+                  let
+                    val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
+                    val th_atts' =
+                      (case dyn' of
+                        NONE => ([th'], [])
+                      | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
+                  in (th_atts', res3) end))
+              |>> flat;
+          in (((b, []), fact'), res') end);
     val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
   in decl_fact :: facts' end;