redundant: default is false;

--- 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