dest/cert_def: replaced Pretty.pp by explicit Proof.context;

--- a/src/Pure/Isar/class.ML	Thu Oct 11 19:10:22 2007 +0200
+++ b/src/Pure/Isar/class.ML	Thu Oct 11 19:10:23 2007 +0200
@@ -218,7 +218,7 @@
   let
     val ctxt = ProofContext.init thy;
     val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
-    val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
+    val ((c, ty), _) = Sign.cert_def ctxt t;
     val atts = map (prep_att thy) raw_atts;
     val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
     val name = case raw_name

--- a/src/Pure/Isar/local_defs.ML	Thu Oct 11 19:10:22 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Oct 11 19:10:23 2007 +0200
@@ -40,12 +40,11 @@
 
 fun cert_def ctxt eq =
   let
-    val pp = Syntax.pp ctxt;
-    val display_term = quote o Pretty.string_of_term pp;
+    val display_term = quote o Syntax.string_of_term ctxt;
     fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     val ((lhs, _), eq') = eq
-      |> Sign.no_vars pp
-      |> PrimitiveDefs.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
+      |> Sign.no_vars (Syntax.pp ctxt)
+      |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 

--- a/src/Pure/primitive_defs.ML	Thu Oct 11 19:10:22 2007 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Oct 11 19:10:23 2007 +0200
@@ -7,7 +7,7 @@
 
 signature PRIMITIVE_DEFS =
 sig
-  val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
+  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
@@ -22,15 +22,15 @@
   | term_kind _ = "";
 
 (*c x == t[x] to !!x. c x == t[x]*)
-fun dest_def pp check_head is_fixed is_fixedT eq =
+fun dest_def ctxt check_head is_fixed is_fixedT eq =
   let
     fun err msg = raise TERM (msg, [eq]);
     val eq_vars = Term.strip_all_vars eq;
     val eq_body = Term.strip_all_body eq;
 
     val display_terms =
-      commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
-    val display_types = commas_quote o map (Pretty.string_of_typ pp);
+      commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
+    val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
 
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
     val lhs = Envir.beta_eta_contract raw_lhs;

--- 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;
 

--- a/src/Pure/theory.ML	Thu Oct 11 19:10:22 2007 +0200
+++ b/src/Pure/theory.ML	Thu Oct 11 19:10:23 2007 +0200
@@ -294,8 +294,9 @@
 
 fun check_def thy unchecked overloaded (bname, tm) defs =
   let
+    val ctxt = ProofContext.init thy;
     val name = Sign.full_name thy bname;
-    val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
+    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end