--- a/src/Pure/Isar/local_defs.ML Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Tue Mar 03 14:07:43 2009 +0100
@@ -11,8 +11,8 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
- Proof.context -> (term * (string * thm)) list * Proof.context
+ val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
+ (term * (string * thm)) list * Proof.context
val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
@@ -104,7 +104,7 @@
end;
fun add_def (var, rhs) ctxt =
- let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
+ let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
in ((lhs, th), ctxt') end;