--- a/src/Pure/Isar/local_defs.ML Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/Isar/local_defs.ML Thu Dec 04 14:43:33 2008 +0100
@@ -12,10 +12,10 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
+ val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
Proof.context -> (term * (string * thm)) list * Proof.context
- val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
- val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
+ val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+ val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
val export: Proof.context -> Proof.context -> thm -> thm list * thm
val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
@@ -92,7 +92,7 @@
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
val xs = map Name.name_of bvars;
- val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
+ val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
@@ -105,7 +105,7 @@
end;
fun add_def (var, rhs) ctxt =
- let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
+ let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
in ((lhs, th), ctxt') end;