# HG changeset patch
# User wenzelm
# Date 1465291621 -7200
# Node ID d1693d7b0c01dd8b886cf723596dfa41269b9966
# Parent  f59fd6cc935e02ee3b548528eb1ccce5ded476b0
tuned;

diff -r f59fd6cc935e -r d1693d7b0c01 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jun 06 21:28:46 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 07 11:27:01 2016 +0200
@@ -315,7 +315,7 @@
     else state
   end;
 
-fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+fun put_goal goal = map_top (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
 
 val set_goal = put_goal o SOME;
 val reset_goal = put_goal NONE;
@@ -553,15 +553,15 @@
 (* goal views -- corresponding to methods *)
 
 fun raw_goal state =
-  let val (ctxt, (facts, goal)) = get_goal state
-  in {context = ctxt, facts = facts, goal = goal} end;
+  let val (ctxt, (using, goal)) = get_goal state
+  in {context = ctxt, facts = using, goal = goal} end;
 
 val goal = raw_goal o refine_insert [];
 
 fun simple_goal state =
   let
-    val (_, (facts, _)) = get_goal state;
-    val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
+    val (_, (using, _)) = get_goal state;
+    val (ctxt, (_, goal)) = get_goal (refine_insert using state);
   in {context = ctxt, goal = goal} end;
 
 fun status_markup state =