--- a/src/Pure/primitive_defs.ML Sat Mar 27 17:36:32 2010 +0100
+++ b/src/Pure/primitive_defs.ML Sat Mar 27 18:07:21 2010 +0100
@@ -9,7 +9,6 @@
val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
term -> (term * term) * term
val abs_def: term -> term * term
- val mk_defpair: term * term -> string * term
end;
structure Primitive_Defs: PRIMITIVE_DEFS =
@@ -78,10 +77,4 @@
val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
in (lhs', rhs') end;
-fun mk_defpair (lhs, rhs) =
- (case Term.head_of lhs of
- Const (name, _) =>
- (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
- | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
-
end;