src/HOL/Import/import_rule.ML

           getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
       | process tstate (#"L", [t, th]) =
           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
             setth th' (thy, state)
           end