src/Pure/Tools/find_theorems.ML
changeset 33290 6dcb0a970783
parent 33095 bbd52d2f8696
child 33301 1fe9fc908ec3
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Oct 28 22:01:40 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 28 22:02:53 2009 +0100
     1.3 @@ -456,7 +456,7 @@
     1.4      let
     1.5        val proof_state = Toplevel.enter_proof_body state;
     1.6        val ctxt = Proof.context_of proof_state;
     1.7 -      val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
     1.8 +      val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
     1.9      in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    1.10  
    1.11  local