--- a/src/Pure/Isar/proof_context.ML Fri Apr 22 15:34:37 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Apr 24 20:29:49 2016 +0200
@@ -166,6 +166,12 @@
val generic_add_abbrev: string -> binding * term -> Context.generic ->
(term * term) * Context.generic
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
+ val cert_spec: (binding * typ option * mixfix) list -> (term * term list) list list ->
+ Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
+ term list list * (indexname * term) list * (indexname * term) list) * Proof.context
+ val read_spec: (binding * string option * mixfix) list -> (string * string list) list list ->
+ Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
+ term list list * (indexname * term) list * (indexname * term) list) * Proof.context
val print_syntax: Proof.context -> unit
val print_abbrevs: bool -> Proof.context -> unit
val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1320,6 +1326,42 @@
end;
+(* specification with parameters *)
+
+local
+
+fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt =
+ let
+ (*vars*)
+ val ((xs', vars), vars_ctxt) = ctxt
+ |> fold_map prep_var raw_vars
+ |-> (fn vars => add_fixes vars ##>> pair vars);
+ val xs = map (Variable.check_name o #1) vars;
+
+ (*propps*)
+ val (propss, binds) = prep_propp vars_ctxt raw_propps;
+ val props = flat propss;
+
+ (*params*)
+ val (ps, params_ctxt) = vars_ctxt
+ |> fold Variable.declare_term props
+ |> fold Variable.bind_term binds
+ |> fold_map inferred_param xs';
+ val params = map Free ps;
+ val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
+ val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
+
+ val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt;
+ in (((vars', xs, params), propss, binds, binds'), params_ctxt) end;
+
+in
+
+val cert_spec = prep_spec cert_var cert_propp;
+val read_spec = prep_spec read_var read_propp;
+
+end;
+
+
(** print context information **)