src/Pure/Isar/calculation.ML

     val state' = put_calculation (SOME calc) state;
     val ctxt' = Proof.context_of state';
     val _ =
       if int then
         Pretty.writeln
-          (ProofContext.pretty_fact ctxt'
-            (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
+          (Proof_Context.pretty_fact ctxt'
+            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
       else ();
   in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
 
 (* also and finally *)