back to Proof.raw_goal;
authorwenzelm
Wed Oct 28 22:04:57 2009 +0100 (2009-10-28)
changeset 3329193f0238151f6
parent 33290 6dcb0a970783
child 33292 affe60b3d864
back to Proof.raw_goal;
src/HOL/Tools/refute_isar.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/refute_isar.ML	Wed Oct 28 22:02:53 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute_isar.ML	Wed Oct 28 22:04:57 2009 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4          Toplevel.keep (fn state =>
     1.5            let
     1.6              val thy = Toplevel.theory_of state;
     1.7 -            val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
     1.8 +            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
     1.9            in Refute.refute_goal thy parms st i end)));
    1.10  
    1.11  
     2.1 --- a/src/Tools/quickcheck.ML	Wed Oct 28 22:02:53 2009 +0100
     2.2 +++ b/src/Tools/quickcheck.ML	Wed Oct 28 22:04:57 2009 +0100
     2.3 @@ -143,7 +143,7 @@
     2.4      val thy = Proof.theory_of state;
     2.5      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
     2.6        | strip t = t;
     2.7 -    val (_, st) = Proof.flat_goal state;
     2.8 +    val {goal = st, ...} = Proof.raw_goal state;
     2.9      val (gi, frees) = Logic.goal_params (prop_of st) i;
    2.10      val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
    2.11        |> monomorphic_term thy insts default_T