src/Pure/Isar/calculation.ML
changeset 6782 adf099e851ed
parent 6781 0db24da2a3c1
child 6787 25265c6807c3
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Jun 04 20:10:07 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Jun 04 22:12:33 1999 +0200
     1.3 @@ -113,12 +113,17 @@
     1.4  
     1.5  (** proof commands **)
     1.6  
     1.7 +fun dest_arg tm =
     1.8 +  (case ObjectLogic.dest_main_statement tm of
     1.9 +    _ $ t => t
    1.10 +  | _ => raise TERM ("dest_arg", [tm]));
    1.11 +
    1.12  val calculationN = "calculation";
    1.13  
    1.14 -fun calculate final prt state =
    1.15 +fun calculate final print state =
    1.16    let
    1.17      val fact = Proof.the_fact state;
    1.18 -    val dddot = ObjectLogic.dest_main_statement (#prop (Thm.rep_thm fact)) handle TERM _ =>
    1.19 +    val dddot = dest_arg (#prop (Thm.rep_thm fact)) handle TERM _ =>
    1.20        raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);
    1.21  
    1.22      val name = if final then "" else calculationN;
    1.23 @@ -130,9 +135,8 @@
    1.24          None => Seq.single fact
    1.25        | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
    1.26    in
    1.27 -    calculations
    1.28 -    |> Seq.map (fn calc =>
    1.29 -      (prt calc;
    1.30 +    calculations |> Seq.map (fn calc =>
    1.31 +      (print calc;
    1.32          state
    1.33          |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
    1.34          |> put_calculation calc
    1.35 @@ -140,8 +144,8 @@
    1.36          |> (if final then Proof.chain else Proof.reset_facts)))
    1.37    end;
    1.38  
    1.39 -fun also prt = calculate false prt;
    1.40 -fun finally prt = calculate true prt;
    1.41 +fun also print = calculate false print;
    1.42 +fun finally print = calculate true print;
    1.43  
    1.44  
    1.45