diff -r dd287c773455 -r 32538cf750ca src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Nov 10 20:57:20 2005 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Nov 10 20:57:21 2005 +0100
@@ -42,8 +42,8 @@
   val obtain_i: (string list * typ option) list ->
     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
     -> bool -> Proof.state -> Proof.state
-  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state Seq.seq
-  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq
+  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state
+  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state
 end;
 
 structure Obtain: OBTAIN =
@@ -110,7 +110,7 @@
     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
 
     fun occs_var x = Library.get_first (fn t =>
-      ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
+      Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
     val raw_parms = map occs_var xs;
     val parms = List.mapPartial I raw_parms;
     val parm_names =
@@ -245,7 +245,7 @@
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
       "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
-    |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis))))
+    |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
   end;
 
 in