# HG changeset patch
# User wenzelm
# Date 1138559030 -3600
# Node ID 23db974a0575220a6cb13f613aca92b4d2884216
# Parent  eb68d3723e84cb2e15f7d9e006db89e16b3f7723
'unfolding': LocalDefs.unfold;

diff -r eb68d3723e84 -r 23db974a0575 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jan 29 19:23:49 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Jan 29 19:23:50 2006 +0100
@@ -632,18 +632,21 @@
   state
   |> assert_backward
   |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
-  |-> (fn named_facts => map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
-    let val ths = List.concat (map snd named_facts)
-    in (statement, f ths using, g ths goal, before_qed, after_qed) end));
+  |> (fn (named_facts, state') =>
+    state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
+      let
+        val ctxt = context_of state';
+        val ths = List.concat (map snd named_facts);
+      in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
 
-fun append_using ths using = using @ ths;
-fun unfold_using ths = map (ObjectLogic.unfold ths);
-val unfold_goals = ObjectLogic.unfold_goals;
+fun append_using _ ths using = using @ ths;
+fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt true ths);
+fun unfold_goals ctxt ths = LocalDefs.unfold_goals ctxt true ths;
 
 in
 
-val using = gen_using append_using (K I) ProofContext.note_thmss Attrib.attribute;
-val using_i = gen_using append_using (K I) ProofContext.note_thmss_i (K I);
+val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
+val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
 val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
 val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);