src/Pure/Isar/obtain.ML
changeset 18151 32538cf750ca
parent 18124 a310c78298f9
child 18185 9d51fad6bb1f
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Nov 10 20:57:20 2005 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Nov 10 20:57:21 2005 +0100
     1.3 @@ -42,8 +42,8 @@
     1.4    val obtain_i: (string list * typ option) list ->
     1.5      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
     1.6      -> bool -> Proof.state -> Proof.state
     1.7 -  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state Seq.seq
     1.8 -  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq
     1.9 +  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state
    1.10 +  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state
    1.11  end;
    1.12  
    1.13  structure Obtain: OBTAIN =
    1.14 @@ -110,7 +110,7 @@
    1.15      val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
    1.16  
    1.17      fun occs_var x = Library.get_first (fn t =>
    1.18 -      ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.19 +      Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.20      val raw_parms = map occs_var xs;
    1.21      val parms = List.mapPartial I raw_parms;
    1.22      val parm_names =
    1.23 @@ -245,7 +245,7 @@
    1.24      |> Proof.chain_facts chain_facts
    1.25      |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
    1.26        "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
    1.27 -    |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis))))
    1.28 +    |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
    1.29    end;
    1.30  
    1.31  in