# HG changeset patch # User wenzelm # Date 1192122623 -7200 # Node ID 4ec3f95190bfdd18cfbc490f67267dc31a3c2662 # Parent 16a74cfca971d89b712a6612deef5a1688d629ed dest/cert_def: replaced Pretty.pp by explicit Proof.context; diff -r 16a74cfca971 -r 4ec3f95190bf src/Pure/Isar/class.ML --- 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 diff -r 16a74cfca971 -r 4ec3f95190bf src/Pure/Isar/local_defs.ML --- 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; diff -r 16a74cfca971 -r 4ec3f95190bf src/Pure/primitive_defs.ML --- 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; 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; diff -r 16a74cfca971 -r 4ec3f95190bf src/Pure/theory.ML --- 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