src/Pure/primitive_defs.ML
changeset 35989 3418cdf1855e
parent 33385 fb2358edcfb6
child 42284 326f57825e1a
     1.1 --- a/src/Pure/primitive_defs.ML	Sat Mar 27 17:36:32 2010 +0100
     1.2 +++ b/src/Pure/primitive_defs.ML	Sat Mar 27 18:07:21 2010 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4    val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     1.5      term -> (term * term) * term
     1.6    val abs_def: term -> term * term
     1.7 -  val mk_defpair: term * term -> string * term
     1.8  end;
     1.9  
    1.10  structure Primitive_Defs: PRIMITIVE_DEFS =
    1.11 @@ -78,10 +77,4 @@
    1.12      val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    1.13    in (lhs', rhs') end;
    1.14  
    1.15 -fun mk_defpair (lhs, rhs) =
    1.16 -  (case Term.head_of lhs of
    1.17 -    Const (name, _) =>
    1.18 -      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    1.19 -  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    1.20 -
    1.21  end;