src/Pure/Isar/obtain.ML
changeset 19585 70a1ce3b23ae
parent 19482 9f11af8f7ef9
child 19779 5c77dfb74c7b
     1.1 --- a/src/Pure/Isar/obtain.ML	Sun May 07 00:21:13 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sun May 07 00:22:05 2006 +0200
     1.3 @@ -40,19 +40,18 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val obtain: string -> (string * string option) list ->
     1.7 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list
     1.8 +    ((string * Attrib.src list) * (string * string list) list) list
     1.9      -> bool -> Proof.state -> Proof.state
    1.10    val obtain_i: string -> (string * typ option) list ->
    1.11 -    ((string * attribute list) * (term * (term list * term list)) list) list
    1.12 +    ((string * attribute list) * (term * term list) list) list
    1.13      -> bool -> Proof.state -> Proof.state
    1.14    val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    1.15    val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    1.16    val statement: (string * ((string * 'typ option) list * 'term list)) list ->
    1.17      (('typ, 'term, 'fact) Element.ctxt list *
    1.18 -      ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) *
    1.19 -    (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context ->
    1.20 -      (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) *
    1.21 -        Proof.context)
    1.22 +      ((string * Attrib.src list) * ('term * 'term list) list) list) *
    1.23 +    (((string * Attrib.src list) * (term * term list) list) list -> Proof.context ->
    1.24 +      (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context)
    1.25  end;
    1.26  
    1.27  structure Obtain: OBTAIN =
    1.28 @@ -151,13 +150,13 @@
    1.29    in
    1.30      state
    1.31      |> Proof.enter_forward
    1.32 -    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
    1.33 +    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
    1.34      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.35      |> Proof.fix_i [(thesisN, NONE)]
    1.36 -    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.37 +    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    1.38      |> `Proof.the_facts
    1.39      ||> Proof.chain_facts chain_facts
    1.40 -    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
    1.41 +    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
    1.42      |-> Proof.refine_insert
    1.43    end;
    1.44  
    1.45 @@ -246,7 +245,7 @@
    1.46          val ps = map dest_Free ts;
    1.47          val asms =
    1.48            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
    1.49 -          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
    1.50 +          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
    1.51          val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
    1.52        in
    1.53          Proof.fix_i (map (apsnd SOME) parms)
    1.54 @@ -285,7 +284,7 @@
    1.55        cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
    1.56      val elems = cases |> map (fn (_, (vars, _)) =>
    1.57        Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.58 -    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
    1.59 +    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props));
    1.60  
    1.61      fun mk_stmt stmt ctxt =
    1.62        let
    1.63 @@ -306,14 +305,14 @@
    1.64            in
    1.65              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    1.66              ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
    1.67 -              [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])]
    1.68 +              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.69              |>> (fn [(_, [th])] => th)
    1.70            end;
    1.71          val (ths, ctxt') = ctxt
    1.72            |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
    1.73            |> fold_map assume_case (cases ~~ stmt)
    1.74            |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.75 -      in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end;
    1.76 +      in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
    1.77    in ((elems, concl), mk_stmt) end;
    1.78  
    1.79  end;