src/Pure/sign.ML
changeset 35988 76ca601c941e
parent 35845 e5980f0ad025
child 36157 2fb3e278a5d7
     1.1 --- a/src/Pure/sign.ML	Sat Mar 27 16:01:45 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 27 17:36:32 2010 +0100
     1.3 @@ -68,7 +68,6 @@
     1.4    val cert_prop: theory -> term -> term
     1.5    val no_frees: Pretty.pp -> term -> term
     1.6    val no_vars: Pretty.pp -> term -> term
     1.7 -  val cert_def: Proof.context -> term -> (string * typ) * term
     1.8    val add_defsort: string -> theory -> theory
     1.9    val add_defsort_i: sort -> theory -> theory
    1.10    val add_types: (binding * int * mixfix) list -> theory -> theory
    1.11 @@ -332,14 +331,6 @@
    1.12  val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
    1.13  val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
    1.14  
    1.15 -fun cert_def ctxt tm =
    1.16 -  let val ((lhs, rhs), _) = tm
    1.17 -    |> no_vars (Syntax.pp ctxt)
    1.18 -    |> Logic.strip_imp_concl
    1.19 -    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
    1.20 -  in (Term.dest_Const (Term.head_of lhs), rhs) end
    1.21 -  handle TERM (msg, _) => error msg;
    1.22 -
    1.23  
    1.24  
    1.25  (** signature extension functions **)  (*exception ERROR/TYPE*)