--- a/src/Pure/sign.ML Thu Oct 11 19:10:22 2007 +0200
+++ b/src/Pure/sign.ML Thu Oct 11 19:10:23 2007 +0200
@@ -134,7 +134,7 @@
val cert_prop: theory -> term -> term
val no_frees: Pretty.pp -> term -> term
val no_vars: Pretty.pp -> term -> term
- val cert_def: Pretty.pp -> term -> (string * typ) * term
+ val cert_def: Proof.context -> term -> (string * typ) * term
val read_class: theory -> xstring -> class
val read_arity: theory -> xstring * string list * string -> arity
val cert_arity: theory -> arity -> arity
@@ -450,11 +450,11 @@
val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
-fun cert_def pp tm =
+fun cert_def ctxt tm =
let val ((lhs, rhs), _) = tm
- |> no_vars pp
+ |> no_vars (Syntax.pp ctxt)
|> Logic.strip_imp_concl
- |> PrimitiveDefs.dest_def pp Term.is_Const (K false) (K false)
+ |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
in (Term.dest_Const (Term.head_of lhs), rhs) end
handle TERM (msg, _) => error msg;