src/Pure/Isar/proof.ML
changeset 67119 acb0807ddb56
parent 65458 cf504b7a7aa7
child 67157 d0657c8b7616
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -68,8 +68,6 @@
     1.4    val presume_cmd: (binding * string option * mixfix) list ->
     1.5      (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
     1.6      state -> state
     1.7 -  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
     1.8 -  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
     1.9    val chain: state -> state
    1.10    val chain_facts: thm list -> state -> state
    1.11    val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    1.12 @@ -679,37 +677,6 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* def *)
    1.17 -
    1.18 -local
    1.19 -
    1.20 -fun gen_def prep_att prep_var prep_binds args state =
    1.21 -  let
    1.22 -    val _ = assert_forward state;
    1.23 -    val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
    1.24 -    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
    1.25 -  in
    1.26 -    state
    1.27 -    |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
    1.28 -    |>> map (fn (x, _, mx) => (x, mx))
    1.29 -    |-> (fn vars =>
    1.30 -      map_context_result (prep_binds false (map swap raw_rhss))
    1.31 -      #-> (fn rhss =>
    1.32 -        let
    1.33 -          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
    1.34 -            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
    1.35 -        in map_context_result (Local_Defs.define defs) end))
    1.36 -    |-> (set_facts o map (#2 o #2))
    1.37 -  end;
    1.38 -
    1.39 -in
    1.40 -
    1.41 -val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
    1.42 -val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
    1.43 -
    1.44 -end;
    1.45 -
    1.46 -
    1.47  
    1.48  (** facts **)
    1.49