src/Pure/Isar/proof.ML
changeset 60379 51d9dcd71ad7
parent 60377 234b7da8542e
child 60381 b568b98fa000
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Jun 07 15:35:49 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Jun 07 20:03:40 2015 +0200
     1.3 @@ -591,15 +591,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_fix prep_vars args =
     1.8 +fun gen_fix prep_var args =
     1.9    assert_forward
    1.10 -  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
    1.11 +  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
    1.12    #> reset_facts;
    1.13  
    1.14  in
    1.15  
    1.16 -val fix = gen_fix Proof_Context.cert_vars;
    1.17 -val fix_cmd = gen_fix Proof_Context.read_vars;
    1.18 +val fix = gen_fix Proof_Context.cert_var;
    1.19 +val fix_cmd = gen_fix Proof_Context.read_var;
    1.20  
    1.21  end;
    1.22  
    1.23 @@ -630,14 +630,14 @@
    1.24  
    1.25  local
    1.26  
    1.27 -fun gen_def prep_att prep_vars prep_binds args state =
    1.28 +fun gen_def prep_att prep_var prep_binds args state =
    1.29    let
    1.30      val _ = assert_forward state;
    1.31      val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
    1.32      val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
    1.33    in
    1.34      state
    1.35 -    |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
    1.36 +    |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
    1.37      |>> map (fn (x, _, mx) => (x, mx))
    1.38      |-> (fn vars =>
    1.39        map_context_result (prep_binds false (map swap raw_rhss))
    1.40 @@ -651,8 +651,8 @@
    1.41  
    1.42  in
    1.43  
    1.44 -val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind;
    1.45 -val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind_cmd;
    1.46 +val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
    1.47 +val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
    1.48  
    1.49  end;
    1.50