diff -r 16a74cfca971 -r 4ec3f95190bf src/Pure/sign.ML
--- 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;