tuned signature;
authorwenzelm
Wed Mar 21 21:24:13 2012 +0100 (2012-03-21)
changeset 470682027ff3136cc
parent 47067 4ef29b0c568f
child 47069 451fc10a81f3
tuned signature;
src/Pure/Isar/bundle.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/bundle.ML	Wed Mar 21 21:06:31 2012 +0100
     1.2 +++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 21:24:13 2012 +0100
     1.3 @@ -103,9 +103,9 @@
     1.4  val includes = gen_includes (K I);
     1.5  val includes_cmd = gen_includes check;
     1.6  
     1.7 -fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.put_facts NONE;
     1.8 +fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
     1.9  fun include_cmd bs =
    1.10 -  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.put_facts NONE;
    1.11 +  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
    1.12  
    1.13  fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
    1.14  fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Mar 21 21:06:31 2012 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 21 21:24:13 2012 +0100
     2.3 @@ -860,7 +860,7 @@
     2.4      fun after_qed witss eqns =
     2.5        (Proof.map_context o Context.proof_map)
     2.6          (note_eqns_register deps witss attrss eqns export export')
     2.7 -      #> Proof.put_facts NONE;
     2.8 +      #> Proof.reset_facts;
     2.9    in
    2.10      state
    2.11      |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
     3.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 21 21:06:31 2012 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 21 21:24:13 2012 +0100
     3.3 @@ -23,7 +23,8 @@
     3.4    val put_thms: bool -> string * thm list option -> state -> state
     3.5    val the_facts: state -> thm list
     3.6    val the_fact: state -> thm
     3.7 -  val put_facts: thm list option -> state -> state
     3.8 +  val set_facts: thm list -> state -> state
     3.9 +  val reset_facts: state -> state
    3.10    val assert_forward: state -> state
    3.11    val assert_chain: state -> state
    3.12    val assert_forward_or_chain: state -> state
    3.13 @@ -231,16 +232,19 @@
    3.14    map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
    3.15    put_thms true (Auto_Bind.thisN, facts);
    3.16  
    3.17 +val set_facts = put_facts o SOME;
    3.18 +val reset_facts = put_facts NONE;
    3.19 +
    3.20  fun these_factss more_facts (named_factss, state) =
    3.21 -  (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
    3.22 +  (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
    3.23  
    3.24  fun export_facts inner outer =
    3.25    (case get_facts inner of
    3.26 -    NONE => put_facts NONE outer
    3.27 +    NONE => reset_facts outer
    3.28    | SOME thms =>
    3.29        thms
    3.30        |> Proof_Context.export (context_of inner) (context_of outer)
    3.31 -      |> (fn ths => put_facts (SOME ths) outer));
    3.32 +      |> (fn ths => set_facts ths outer));
    3.33  
    3.34  
    3.35  (* mode *)
    3.36 @@ -283,6 +287,9 @@
    3.37  
    3.38  fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
    3.39  
    3.40 +val set_goal = put_goal o SOME;
    3.41 +val reset_goal = put_goal NONE;
    3.42 +
    3.43  val before_qed = #before_qed o #2 o current_goal;
    3.44  
    3.45  
    3.46 @@ -298,7 +305,7 @@
    3.47        in map_context f (State (nd, node' :: nodes')) end
    3.48    | map_goal _ _ state = state;
    3.49  
    3.50 -fun set_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
    3.51 +fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
    3.52    (statement, [], using, goal, before_qed, after_qed));
    3.53  
    3.54  fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
    3.55 @@ -412,10 +419,10 @@
    3.56    |> ALLGOALS Goal.conjunction_tac
    3.57    |> Seq.maps (fn goal =>
    3.58      state
    3.59 -    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
    3.60 +    |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
    3.61      |> Seq.maps meth
    3.62      |> Seq.maps (fn state' => state'
    3.63 -      |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
    3.64 +      |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
    3.65      |> Seq.maps (apply_method true (K Method.succeed)));
    3.66  
    3.67  fun apply_text cc text state =
    3.68 @@ -471,7 +478,7 @@
    3.69    in
    3.70      raw_rules
    3.71      |> Proof_Context.goal_export inner outer
    3.72 -    |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
    3.73 +    |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
    3.74    end;
    3.75  
    3.76  end;
    3.77 @@ -548,7 +555,7 @@
    3.78    state
    3.79    |> assert_forward
    3.80    |> map_context (bind true args #> snd)
    3.81 -  |> put_facts NONE;
    3.82 +  |> reset_facts;
    3.83  
    3.84  in
    3.85  
    3.86 @@ -565,7 +572,7 @@
    3.87  fun gen_write prep_arg mode args =
    3.88    assert_forward
    3.89    #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
    3.90 -  #> put_facts NONE;
    3.91 +  #> reset_facts;
    3.92  
    3.93  in
    3.94  
    3.95 @@ -585,7 +592,7 @@
    3.96  fun gen_fix prep_vars args =
    3.97    assert_forward
    3.98    #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
    3.99 -  #> put_facts NONE;
   3.100 +  #> reset_facts;
   3.101  
   3.102  in
   3.103  
   3.104 @@ -635,7 +642,7 @@
   3.105      |-> (fn vars =>
   3.106        map_context_result (prep_binds false (map swap raw_rhss))
   3.107        #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
   3.108 -    |-> (put_facts o SOME o map (#2 o #2))
   3.109 +    |-> (set_facts o map (#2 o #2))
   3.110    end;
   3.111  
   3.112  in
   3.113 @@ -652,7 +659,7 @@
   3.114  (* chain *)
   3.115  
   3.116  fun clean_facts ctxt =
   3.117 -  put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
   3.118 +  set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
   3.119  
   3.120  val chain =
   3.121    assert_forward
   3.122 @@ -660,7 +667,7 @@
   3.123    #> enter_chain;
   3.124  
   3.125  fun chain_facts facts =
   3.126 -  put_facts (SOME facts)
   3.127 +  set_facts facts
   3.128    #> chain;
   3.129  
   3.130  
   3.131 @@ -765,15 +772,15 @@
   3.132  val begin_block =
   3.133    assert_forward
   3.134    #> open_block
   3.135 -  #> put_goal NONE
   3.136 +  #> reset_goal
   3.137    #> open_block;
   3.138  
   3.139  val next_block =
   3.140    assert_forward
   3.141    #> close_block
   3.142    #> open_block
   3.143 -  #> put_goal NONE
   3.144 -  #> put_facts NONE;
   3.145 +  #> reset_goal
   3.146 +  #> reset_facts;
   3.147  
   3.148  fun end_block state =
   3.149    state
   3.150 @@ -889,12 +896,12 @@
   3.151    in
   3.152      goal_state
   3.153      |> map_context (init_context #> Variable.set_body true)
   3.154 -    |> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
   3.155 +    |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
   3.156      |> map_context (Proof_Context.auto_bind_goal props)
   3.157      |> chaining ? (`the_facts #-> using_facts)
   3.158 -    |> put_facts NONE
   3.159 +    |> reset_facts
   3.160      |> open_block
   3.161 -    |> put_goal NONE
   3.162 +    |> reset_goal
   3.163      |> enter_backward
   3.164      |> not (null vars) ? refine_terms (length goal_propss)
   3.165      |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)