refine_end;
authorwenzelm
Sun Feb 13 20:54:12 2000 +0100 (2000-02-13)
changeset 823436a85a6c4852
parent 8233 85169951d515
child 8235 a4fb9be6b19a
refine_end;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Feb 13 20:52:58 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Feb 13 20:54:12 2000 +0100
     1.3 @@ -42,6 +42,7 @@
     1.4    type method
     1.5    val method: (thm list -> tactic) -> method
     1.6    val refine: (context -> method) -> state -> state Seq.seq
     1.7 +  val refine_end: (context -> method) -> state -> state Seq.seq
     1.8    val find_free: term -> string -> term option
     1.9    val export_thm: context -> thm -> thm
    1.10    val match_bind: (string list * string) list -> state -> state
    1.11 @@ -346,14 +347,16 @@
    1.12  
    1.13  (* refine goal *)
    1.14  
    1.15 +local
    1.16 +
    1.17  fun check_sign sg state =
    1.18    if Sign.subsig (sg, sign_of state) then state
    1.19    else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
    1.20  
    1.21 -fun refine meth_fun state =
    1.22 +fun gen_refine current_context meth_fun state =
    1.23    let
    1.24 -    val Method meth = meth_fun (context_of state);
    1.25 -    val (_, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
    1.26 +    val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
    1.27 +    val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
    1.28  
    1.29      fun refn thm' =
    1.30        state
    1.31 @@ -361,6 +364,13 @@
    1.32        |> map_goal (K ((result, (facts, thm')), f));
    1.33    in Seq.map refn (meth facts thm) end;
    1.34  
    1.35 +in
    1.36 +
    1.37 +val refine = gen_refine true;
    1.38 +val refine_end = gen_refine false;
    1.39 +
    1.40 +end;
    1.41 +
    1.42  
    1.43  (* export *)
    1.44