src/Pure/Isar/local_defs.ML
changeset 28083 103d9282a946
parent 26424 a6cad32a27b0
child 28965 1de908189869
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -12,10 +12,11 @@
     1.4    val mk_def: Proof.context -> (string * term) list -> term list
     1.5    val expand: cterm list -> thm -> thm
     1.6    val def_export: Assumption.export
     1.7 -  val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     1.8 -    (term * (bstring * thm)) list * Proof.context
     1.9 -  val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
    1.10 -  val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
    1.11 +  val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
    1.12 +    Proof.context -> (term * (string * thm)) list * Proof.context
    1.13 +  val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
    1.14 +  val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
    1.15 +    (term * term) * Proof.context
    1.16    val export: Proof.context -> Proof.context -> thm -> thm list * thm
    1.17    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
    1.18    val trans_terms: Proof.context -> thm list -> thm
    1.19 @@ -88,22 +89,23 @@
    1.20  
    1.21  fun add_defs defs ctxt =
    1.22    let
    1.23 -    val ((xs, mxs), specs) = defs |> split_list |>> split_list;
    1.24 -    val ((names, atts), rhss) = specs |> split_list |>> split_list;
    1.25 -    val names' = map2 Thm.def_name_optional xs names;
    1.26 +    val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
    1.27 +    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    1.28 +    val xs = map Name.name_of bvars;
    1.29 +    val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
    1.30      val eqs = mk_def ctxt (xs ~~ rhss);
    1.31      val lhss = map (fst o Logic.dest_equals) eqs;
    1.32    in
    1.33      ctxt
    1.34 -    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
    1.35 +    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
    1.36      |> fold Variable.declare_term eqs
    1.37      |> ProofContext.add_assms_i def_export
    1.38 -      (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
    1.39 +      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
    1.40      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
    1.41    end;
    1.42  
    1.43  fun add_def (var, rhs) ctxt =
    1.44 -  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
    1.45 +  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
    1.46    in ((lhs, th), ctxt') end;
    1.47  
    1.48