# HG changeset patch
# User wenzelm
# Date 1576765788 -3600
# Node ID 1be996d8bb982416c4e177bdb3db46b87243735f
# Parent  e58bc223f46c225040e8a4830107123cfb6e3a26
proper proof body context for Simplifier plugins (solvers, loopers, ...) -- avoid crash due to Subgoal.FOCUS (before e58bc223f46c);

diff -r e58bc223f46c -r 1be996d8bb98 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Dec 19 15:22:35 2019 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Dec 19 15:29:48 2019 +0100
@@ -1350,6 +1350,7 @@
 
     val ctxt =
       raw_ctxt
+      |> Variable.set_body true
       |> Context_Position.set_visible false
       |> inc_simp_depth
       |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);