tuned;
authorwenzelm
Wed Jan 05 11:45:31 2000 +0100 (2000-01-05)
changeset 8095497a9240acf3
parent 8094 62b45a2e6ecb
child 8096 4da940d100f5
tuned;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 05 11:45:01 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jan 05 11:45:31 2000 +0100
     1.3 @@ -491,8 +491,8 @@
     1.4    |> map_context (f x)
     1.5    |> reset_facts;
     1.6  
     1.7 -val match_bind = gen_bind ProofContext.match_binds;
     1.8 -val match_bind_i = gen_bind ProofContext.match_binds_i;
     1.9 +val match_bind = gen_bind ProofContext.match_bind;
    1.10 +val match_bind_i = gen_bind ProofContext.match_bind_i;
    1.11  
    1.12  
    1.13  (* have_thmss *)
    1.14 @@ -577,7 +577,7 @@
    1.15        state
    1.16        |> assert_forward_or_chain
    1.17        |> enter_forward
    1.18 -      |> map_context_result (prepp raw_propp);
    1.19 +      |> map_context_result (fn ct => prepp (ct, raw_propp));
    1.20      val cprop = Thm.cterm_of (sign_of state') prop;
    1.21      val goal = Drule.mk_triv_goal cprop;
    1.22    in
    1.23 @@ -592,8 +592,8 @@
    1.24  
    1.25  
    1.26  (*global goals*)
    1.27 -fun global_goal prep kind name atts x thy =
    1.28 -  setup_goal I prep kind Seq.single name atts x (init_state thy);
    1.29 +fun global_goal prepp kind name atts x thy =
    1.30 +  setup_goal I prepp kind Seq.single name atts x (init_state thy);
    1.31  
    1.32  val theorem = global_goal ProofContext.bind_propp Theorem;
    1.33  val theorem_i = global_goal ProofContext.bind_propp_i Theorem;
    1.34 @@ -602,9 +602,9 @@
    1.35  
    1.36  
    1.37  (*local goals*)
    1.38 -fun local_goal prep kind f name atts args state =
    1.39 +fun local_goal prepp kind f name atts args state =
    1.40    state
    1.41 -  |> setup_goal open_block prep kind f name atts args
    1.42 +  |> setup_goal open_block prepp kind f name atts args
    1.43    |> warn_extra_tfrees state;
    1.44  
    1.45  val show   = local_goal ProofContext.bind_propp Goal;