1.1 --- a/src/Pure/primitive_defs.ML	Thu Oct 11 19:10:22 2007 +0200
     1.2 +++ b/src/Pure/primitive_defs.ML	Thu Oct 11 19:10:23 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature PRIMITIVE_DEFS =
     1.6  sig
     1.7 -  val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     1.8 +  val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     1.9      term -> (term * term) * term
    1.10    val abs_def: term -> term * term
    1.11    val mk_defpair: term * term -> string * term
    1.12 @@ -22,15 +22,15 @@
    1.13    | term_kind _ = "";
    1.14  
    1.15  (*c x == t[x] to !!x. c x == t[x]*)
    1.16 -fun dest_def pp check_head is_fixed is_fixedT eq =
    1.17 +fun dest_def ctxt check_head is_fixed is_fixedT eq =
    1.18    let
    1.19      fun err msg = raise TERM (msg, [eq]);
    1.20      val eq_vars = Term.strip_all_vars eq;
    1.21      val eq_body = Term.strip_all_body eq;
    1.22  
    1.23      val display_terms =
    1.24 -      commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
    1.25 -    val display_types = commas_quote o map (Pretty.string_of_typ pp);
    1.26 +      commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
    1.27 +    val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
    1.28  
    1.29      val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
    1.30      val lhs = Envir.beta_eta_contract raw_lhs;