src/Pure/Isar/proof.ML
changeset 7478 02291239d627
parent 7412 35ebe1452c10
child 7487 c0f9b956a3e7
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Sep 04 21:07:12 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Sep 04 21:08:38 1999 +0200
     1.3 @@ -273,7 +273,7 @@
     1.4  
     1.5  fun close_block (state as State (_, node :: nodes)) =
     1.6        State (node, nodes)
     1.7 -      |> map_context (ProofContext.transfer_used_names (context_of state))
     1.8 +(* FIXME      |> map_context (ProofContext.transfer_used_names (context_of state)) *)
     1.9    | close_block state = raise STATE ("Unbalanced block parentheses", state);
    1.10  
    1.11  
    1.12 @@ -508,7 +508,7 @@
    1.13  fun have_thmss ths name atts ths_atts state =
    1.14    state
    1.15    |> assert_forward
    1.16 -  |> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts)
    1.17 +  |> map_context_result (ProofContext.have_thmss ths name atts ths_atts)
    1.18    |> these_facts;
    1.19  
    1.20  fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
    1.21 @@ -530,12 +530,10 @@
    1.22  
    1.23  local
    1.24  
    1.25 -fun def_name (name, x, y) = (PureThy.default_name name, x, y);
    1.26 -
    1.27  fun gen_assume f tac args state =
    1.28    state
    1.29    |> assert_forward
    1.30 -  |> map_context_result (f tac (map def_name args))
    1.31 +  |> map_context_result (f tac args)
    1.32    |> (fn (st, (factss, prems)) =>
    1.33      foldl these_facts (st, factss)
    1.34      |> put_thms ("prems", prems)
    1.35 @@ -597,7 +595,7 @@
    1.36    in
    1.37      state'
    1.38      |> opt_block
    1.39 -    |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed))
    1.40 +    |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed))
    1.41      |> auto_bind_goal prop
    1.42      |> (if is_chain state then use_facts else reset_facts)
    1.43      |> new_block