tuned;
authorwenzelm
Sat Jun 05 20:32:10 1999 +0200 (1999-06-05)
changeset 678725265c6807c3
parent 6786 0af1797d5315
child 6788 6eaf6856ee4a
tuned;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Sat Jun 05 20:30:29 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sat Jun 05 20:32:10 1999 +0200
     1.3 @@ -58,20 +58,23 @@
     1.4  end;
     1.5  
     1.6  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
     1.7 -val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
     1.8 +val get_local_rules = #1 o LocalCalculation.get_st;
     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 (Proof.context_of state)) of
    1.16 +  (case #2 (LocalCalculation.get_st state) of
    1.17      None => None
    1.18    | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
    1.19  
    1.20  fun put_calculation thm state =
    1.21    LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
    1.22  
    1.23 +fun reset_calculation state =
    1.24 +  LocalCalculation.put_st (get_local_rules state, None) state;
    1.25 +
    1.26  
    1.27  
    1.28  (** attributes **)
    1.29 @@ -111,24 +114,16 @@
    1.30    (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
    1.31  
    1.32  
    1.33 +
    1.34  (** proof commands **)
    1.35  
    1.36 -fun dest_arg tm =
    1.37 -  (case ObjectLogic.dest_main_statement tm of
    1.38 -    _ $ t => t
    1.39 -  | _ => raise TERM ("dest_arg", [tm]));
    1.40 +fun have_thms name thms = Proof.have_thmss name [] [(thms, [])];
    1.41  
    1.42  val calculationN = "calculation";
    1.43  
    1.44  fun calculate final print state =
    1.45    let
    1.46      val fact = Proof.the_fact state;
    1.47 -    val dddot = dest_arg (#prop (Thm.rep_thm fact)) handle TERM _ =>
    1.48 -      raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);
    1.49 -
    1.50 -    val name = if final then "" else calculationN;
    1.51 -    fun have_thm thm = Proof.have_thmss name [] [([thm], [])];
    1.52 -
    1.53      val rules = Seq.of_list (get_local_rules state);
    1.54      val calculations =
    1.55        (case get_calculation state of
    1.56 @@ -137,11 +132,17 @@
    1.57    in
    1.58      calculations |> Seq.map (fn calc =>
    1.59        (print calc;
    1.60 -        state
    1.61 -        |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
    1.62 -        |> put_calculation calc
    1.63 -        |> have_thm calc
    1.64 -        |> (if final then Proof.chain else Proof.reset_facts)))
    1.65 +        (if final then
    1.66 +          state
    1.67 +          |> reset_calculation
    1.68 +          |> have_thms calculationN []
    1.69 +          |> have_thms "" [calc]
    1.70 +          |> Proof.chain
    1.71 +        else
    1.72 +          state
    1.73 +          |> put_calculation calc
    1.74 +          |> have_thms calculationN [calc]
    1.75 +          |> Proof.reset_facts)))
    1.76    end;
    1.77  
    1.78  fun also print = calculate false print;