# HG changeset patch
# User wenzelm
# Date 1559554043 -7200
# Node ID 502749883f535013110299189a043359ff0c8da9
# Parent  9ea7081c3f03533fa4ec5fd7dbc1bd26d31c05a3
redundant: default is false;

diff -r 9ea7081c3f03 -r 502749883f53 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Jun 01 21:43:41 2019 +0200
+++ b/src/HOL/Import/import_rule.ML	Mon Jun 03 11:27:23 2019 +0200
@@ -373,7 +373,7 @@
           gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
       | process (thy, state) (#"M", [s]) =
           let
-            val ctxt = Variable.set_body false (Proof_Context.init_global thy)
+            val ctxt = Proof_Context.init_global thy
             val thm = freezeT thy (Global_Theory.get_thm thy s)
             val ((_, [th']), _) = Variable.import true [thm] ctxt
           in