src/Pure/Isar/proof.ML
changeset 47815 43f677b3ae91
parent 47431 d9dd4a9f18fc
child 49011 9c68e43502ce
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4    val apply: Method.text -> state -> state Seq.seq
     1.5    val apply_end: Method.text -> state -> state Seq.seq
     1.6    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     1.7 -    (theory -> 'a -> attribute) ->
     1.8 +    (Proof.context -> 'a -> attribute) ->
     1.9      ('b list -> context -> (term list list * (context -> context)) * context) ->
    1.10      string -> Method.text option -> (thm list list -> state -> state) ->
    1.11      ((binding * 'a list) * 'b) list -> state -> state
    1.12 @@ -400,7 +400,8 @@
    1.13  fun no_goal_cases st = map (rpair NONE) (goals st);
    1.14  
    1.15  fun goal_cases st =
    1.16 -  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    1.17 +  Rule_Cases.make_common
    1.18 +    (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    1.19  
    1.20  fun apply_method current_context meth state =
    1.21    let
    1.22 @@ -612,13 +613,13 @@
    1.23  fun gen_assume asm prep_att exp args state =
    1.24    state
    1.25    |> assert_forward
    1.26 -  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
    1.27 +  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
    1.28    |> these_factss [] |> #2;
    1.29  
    1.30  in
    1.31  
    1.32  val assm = gen_assume Proof_Context.add_assms_i (K I);
    1.33 -val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
    1.34 +val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
    1.35  val assume = assm Assumption.assume_export;
    1.36  val assume_cmd = assm_cmd Assumption.assume_export;
    1.37  val presume = assm Assumption.presume_export;
    1.38 @@ -634,10 +635,8 @@
    1.39  fun gen_def prep_att prep_vars prep_binds args state =
    1.40    let
    1.41      val _ = assert_forward state;
    1.42 -    val thy = theory_of state;
    1.43 -
    1.44      val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
    1.45 -    val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
    1.46 +    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
    1.47    in
    1.48      state
    1.49      |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
    1.50 @@ -651,7 +650,7 @@
    1.51  in
    1.52  
    1.53  val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
    1.54 -val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
    1.55 +val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
    1.56  
    1.57  end;
    1.58  
    1.59 @@ -683,10 +682,8 @@
    1.60  fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
    1.61    state
    1.62    |> assert_forward
    1.63 -  |> map_context_result (Proof_Context.note_thmss ""
    1.64 -    (Attrib.map_facts_refs
    1.65 -      (map (prep_atts (theory_of state)))
    1.66 -      (prep_fact (context_of state)) args))
    1.67 +  |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
    1.68 +    (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
    1.69    |> these_factss (more_facts state)
    1.70    ||> opt_chain
    1.71    |> opt_result;
    1.72 @@ -694,13 +691,15 @@
    1.73  in
    1.74  
    1.75  val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
    1.76 -val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
    1.77 +val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
    1.78  
    1.79  val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
    1.80 -val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
    1.81 +val from_thmss_cmd =
    1.82 +  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
    1.83  
    1.84  val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
    1.85 -val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
    1.86 +val with_thmss_cmd =
    1.87 +  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
    1.88  
    1.89  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
    1.90  
    1.91 @@ -715,9 +714,8 @@
    1.92    state
    1.93    |> assert_backward
    1.94    |> map_context_result
    1.95 -    (Proof_Context.note_thmss ""
    1.96 -      (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
    1.97 -        (no_binding args)))
    1.98 +    (fn ctxt => ctxt |> Proof_Context.note_thmss ""
    1.99 +      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   1.100    |> (fn (named_facts, state') =>
   1.101      state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
   1.102        let
   1.103 @@ -732,9 +730,9 @@
   1.104  in
   1.105  
   1.106  val using = gen_using append_using (K (K I)) (K I) (K I);
   1.107 -val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
   1.108 +val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
   1.109  val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
   1.110 -val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
   1.111 +val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
   1.112  
   1.113  end;
   1.114  
   1.115 @@ -748,7 +746,7 @@
   1.116  
   1.117  fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   1.118    let
   1.119 -    val atts = map (prep_att (theory_of state)) raw_atts;
   1.120 +    val atts = map (prep_att (context_of state)) raw_atts;
   1.121      val (asms, state') = state |> map_context_result (fn ctxt =>
   1.122        ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
   1.123      val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   1.124 @@ -762,7 +760,7 @@
   1.125  in
   1.126  
   1.127  val invoke_case = gen_invoke_case (K I);
   1.128 -val invoke_case_cmd = gen_invoke_case Attrib.attribute;
   1.129 +val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
   1.130  
   1.131  end;
   1.132  
   1.133 @@ -935,9 +933,8 @@
   1.134  
   1.135  fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   1.136    let
   1.137 -    val thy = theory_of state;
   1.138      val ((names, attss), propp) =
   1.139 -      Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
   1.140 +      Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
   1.141  
   1.142      fun after_qed' results =
   1.143        local_results ((names ~~ attss) ~~ results)
   1.144 @@ -1044,9 +1041,9 @@
   1.145  in
   1.146  
   1.147  val have = gen_have (K I) Proof_Context.bind_propp_i;
   1.148 -val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
   1.149 +val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
   1.150  val show = gen_show (K I) Proof_Context.bind_propp_i;
   1.151 -val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
   1.152 +val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
   1.153  
   1.154  end;
   1.155