replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
authorwenzelm
Fri Oct 02 22:02:11 2009 +0200 (2009-10-02)
changeset 32859204f749f35a9
parent 32858 51fda1c8fa2d
child 32860 a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
src/Pure/Isar/isar_cmd.ML
src/Pure/Tools/find_theorems.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 02 21:42:31 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 02 22:02:11 2009 +0200
     1.3 @@ -450,14 +450,15 @@
     1.4    Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
     1.5  
     1.6  fun string_of_prfs full state arg =
     1.7 -  Pretty.string_of (case arg of
     1.8 +  Pretty.string_of
     1.9 +    (case arg of
    1.10        NONE =>
    1.11          let
    1.12 -          val (ctxt, (_, thm)) = Proof.get_goal state;
    1.13 +          val (ctxt, thm) = Proof.flat_goal state;
    1.14            val thy = ProofContext.theory_of ctxt;
    1.15            val prf = Thm.proof_of thm;
    1.16            val prop = Thm.full_prop_of thm;
    1.17 -          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
    1.18 +          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
    1.19          in
    1.20            ProofSyntax.pretty_proof ctxt
    1.21              (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Oct 02 21:42:31 2009 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Oct 02 22:02:11 2009 +0200
     2.3 @@ -434,7 +434,7 @@
     2.4      let
     2.5        val proof_state = Toplevel.enter_proof_body state;
     2.6        val ctxt = Proof.context_of proof_state;
     2.7 -      val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
     2.8 +      val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
     2.9      in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    2.10  
    2.11  local
     3.1 --- a/src/Tools/quickcheck.ML	Fri Oct 02 21:42:31 2009 +0200
     3.2 +++ b/src/Tools/quickcheck.ML	Fri Oct 02 22:02:11 2009 +0200
     3.3 @@ -143,7 +143,7 @@
     3.4      val thy = Proof.theory_of state;
     3.5      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
     3.6        | strip t = t;
     3.7 -    val (_, (_, st)) = Proof.get_goal state;
     3.8 +    val (_, st) = Proof.flat_goal state;
     3.9      val (gi, frees) = Logic.goal_params (prop_of st) i;
    3.10      val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
    3.11        |> monomorphic_term thy insts default_T