src/Pure/Isar/proof.ML
changeset 68865 dd44e31ca2c6
parent 68130 6fb85346cb79
child 68875 7f0151c951e3
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Aug 31 16:17:30 2018 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Aug 31 22:25:58 2018 +0200
     1.3 @@ -237,7 +237,7 @@
     1.4  fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
     1.5  
     1.6  fun propagate_ml_env state = map_contexts
     1.7 -  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
     1.8 +  (Context.proof_map (ML_Env.inherit [Context.Proof (context_of state)])) state;
     1.9  
    1.10  
    1.11  (* facts *)