# HG changeset patch
# User wenzelm
# Date 1026837516 -7200
# Node ID 82a057cf441304432bd838d0eb31fd87176d49bf
# Parent  3ec0d8c8beba67c0155b52a72b18580aa790b7f1
avoid "_st" versions of proof data;

diff -r 3ec0d8c8beba -r 82a057cf4413 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Jul 16 18:38:11 2002 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Jul 16 18:38:36 2002 +0200
@@ -70,22 +70,23 @@
 end;
 
 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
-val get_local_rules = #1 o LocalCalculation.get_st;
+val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
 val print_local_rules = LocalCalculation.print;
 
 
 (* access calculation *)
 
 fun get_calculation state =
-  (case #2 (LocalCalculation.get_st state) of
+  (case #2 (LocalCalculation.get (Proof.context_of state)) of
     None => None
   | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
 
 fun put_calculation thms state =
-  LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
+  Proof.map_context
+    (LocalCalculation.put (get_local_rules state, Some (thms, Proof.level state))) state;
 
 fun reset_calculation state =
-  LocalCalculation.put_st (get_local_rules state, None) state;
+  Proof.map_context (LocalCalculation.put (get_local_rules state, None)) state;