redundant: default is false;
authorwenzelm
Mon Jun 03 11:27:23 2019 +0200 (6 weeks ago)
changeset 70303502749883f53
parent 70302 9ea7081c3f03
child 70304 1514efa1e57a
redundant: default is false;
src/HOL/Import/import_rule.ML
     1.1 --- a/src/HOL/Import/import_rule.ML	Sat Jun 01 21:43:41 2019 +0200
     1.2 +++ b/src/HOL/Import/import_rule.ML	Mon Jun 03 11:27:23 2019 +0200
     1.3 @@ -373,7 +373,7 @@
     1.4            gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
     1.5        | process (thy, state) (#"M", [s]) =
     1.6            let
     1.7 -            val ctxt = Variable.set_body false (Proof_Context.init_global thy)
     1.8 +            val ctxt = Proof_Context.init_global thy
     1.9              val thm = freezeT thy (Global_Theory.get_thm thy s)
    1.10              val ((_, [th']), _) = Variable.import true [thm] ctxt
    1.11            in