src/Pure/Isar/proof.ML
changeset 7924 5fee69b1f5fe
parent 7669 fcd9c2050836
child 7928 06a11f8cf573
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Oct 22 21:48:50 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Oct 22 21:49:33 1999 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val context_of: state -> context
     1.5    val theory_of: state -> theory
     1.6    val sign_of: state -> Sign.sg
     1.7 +  val warn_extra_tfrees: state -> state -> state
     1.8    val reset_thms: string -> state -> state
     1.9    val the_facts: state -> thm list
    1.10    val get_goal: state -> term * (thm list * thm)
    1.11 @@ -35,8 +36,6 @@
    1.12    val refine: (context -> method) -> state -> state Seq.seq
    1.13    val find_free: term -> string -> term option
    1.14    val export_thm: context -> thm -> thm
    1.15 -  val bind: (indexname * string) list -> state -> state
    1.16 -  val bind_i: (indexname * term) list -> state -> state
    1.17    val match_bind: (string list * string) list -> state -> state
    1.18    val match_bind_i: (term list * term) list -> state -> state
    1.19    val have_thmss: thm list -> string -> context attribute list ->
    1.20 @@ -179,8 +178,7 @@
    1.21  
    1.22  
    1.23  fun put_data kind f = map_context o ProofContext.put_data kind f;
    1.24 -val declare_term = map_context o ProofContext.declare_term;
    1.25 -val add_binds = map_context o ProofContext.add_binds_i;
    1.26 +val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of;
    1.27  val auto_bind_goal = map_context o ProofContext.auto_bind_goal;
    1.28  val auto_bind_facts = map_context oo ProofContext.auto_bind_facts;
    1.29  val put_thms = map_context o ProofContext.put_thms;
    1.30 @@ -493,9 +491,6 @@
    1.31    |> map_context (f x)
    1.32    |> reset_facts;
    1.33  
    1.34 -val bind = gen_bind (ProofContext.add_binds o map (apsnd Some))
    1.35 -val bind_i = gen_bind (ProofContext.add_binds_i o map (apsnd Some))
    1.36 -
    1.37  val match_bind = gen_bind ProofContext.match_binds;
    1.38  val match_bind_i = gen_bind ProofContext.match_binds_i;
    1.39  
    1.40 @@ -578,11 +573,11 @@
    1.41  
    1.42  fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
    1.43    let
    1.44 -    val (state', prop) =
    1.45 +    val (state', [prop]) =
    1.46        state
    1.47        |> assert_forward_or_chain
    1.48        |> enter_forward
    1.49 -      |> map_context_result (fn c => prepp (c, raw_propp));
    1.50 +      |> map_context_result (prepp [raw_propp]);
    1.51      val cprop = Thm.cterm_of (sign_of state') prop;
    1.52      val goal = Drule.mk_triv_goal cprop;
    1.53    in
    1.54 @@ -598,22 +593,22 @@
    1.55  
    1.56  (*global goals*)
    1.57  fun global_goal prep kind name atts x thy =
    1.58 -  setup_goal I prep kind Seq.single name atts x (init_state thy);
    1.59 +  setup_goal I (prep false) kind Seq.single name atts x (init_state thy);
    1.60  
    1.61 -val theorem = global_goal ProofContext.bind_propp Theorem;
    1.62 -val theorem_i = global_goal ProofContext.bind_propp_i Theorem;
    1.63 -val lemma = global_goal ProofContext.bind_propp Lemma;
    1.64 -val lemma_i = global_goal ProofContext.bind_propp_i Lemma;
    1.65 +val theorem = global_goal ProofContext.bind_propps Theorem;
    1.66 +val theorem_i = global_goal ProofContext.bind_propps_i Theorem;
    1.67 +val lemma = global_goal ProofContext.bind_propps Lemma;
    1.68 +val lemma_i = global_goal ProofContext.bind_propps_i Lemma;
    1.69  
    1.70  
    1.71  (*local goals*)
    1.72  fun local_goal prep kind f name atts x =
    1.73 -  setup_goal open_block prep kind f name atts x;
    1.74 +  setup_goal open_block (prep true) kind f name atts x;
    1.75  
    1.76 -val show   = local_goal ProofContext.bind_propp Goal;
    1.77 -val show_i = local_goal ProofContext.bind_propp_i Goal;
    1.78 -val have   = local_goal ProofContext.bind_propp Aux;
    1.79 -val have_i = local_goal ProofContext.bind_propp_i Aux;
    1.80 +val show   = local_goal ProofContext.bind_propps Goal;
    1.81 +val show_i = local_goal ProofContext.bind_propps_i Goal;
    1.82 +val have   = local_goal ProofContext.bind_propps Aux;
    1.83 +val have_i = local_goal ProofContext.bind_propps_i Aux;
    1.84  
    1.85  
    1.86