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;