1.1 --- a/src/Pure/Isar/calculation.ML	Tue Jul 16 18:38:11 2002 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Jul 16 18:38:36 2002 +0200
     1.3 @@ -70,22 +70,23 @@
     1.4  end;
     1.5  
     1.6  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
     1.7 -val get_local_rules = #1 o LocalCalculation.get_st;
     1.8 +val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
     1.9  val print_local_rules = LocalCalculation.print;
    1.10  
    1.11  
    1.12  (* access calculation *)
    1.13  
    1.14  fun get_calculation state =
    1.15 -  (case #2 (LocalCalculation.get_st state) of
    1.16 +  (case #2 (LocalCalculation.get (Proof.context_of state)) of
    1.17      None => None
    1.18    | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    1.19  
    1.20  fun put_calculation thms state =
    1.21 -  LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    1.22 +  Proof.map_context
    1.23 +    (LocalCalculation.put (get_local_rules state, Some (thms, Proof.level state))) state;
    1.24  
    1.25  fun reset_calculation state =
    1.26 -  LocalCalculation.put_st (get_local_rules state, None) state;
    1.27 +  Proof.map_context (LocalCalculation.put (get_local_rules state, None)) state;
    1.28  
    1.29  
    1.30