--- a/src/Pure/Isar/proof_context.ML Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 26 16:20:28 2016 +0200
@@ -166,12 +166,14 @@
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 cert_statement:
+ (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * term)) list * term list list *
+ (indexname * term) list * (indexname * term) list) * Proof.context
+ val read_statement:
+ (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * 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
@@ -1326,38 +1328,32 @@
end;
-(* specification with parameters *)
+(* structured statement *)
local
-fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt =
+fun prep_statement 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 (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
val xs = map (Variable.check_name o #1) vars;
-
- (*propps*)
- val (propss, binds) = prep_propp vars_ctxt raw_propps;
- val props = flat propss;
+ val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
- (*params*)
- val (ps, params_ctxt) = vars_ctxt
- |> fold Variable.declare_term props
- |> fold Variable.bind_term binds
+ val (propss, binds) = prep_propp fixes_ctxt raw_propps;
+ val (ps, params_ctxt) = fixes_ctxt
+ |> (fold o fold) Variable.declare_term propss
|> 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 params = xs ~~ map Free ps;
+
val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
+ val binds' = (map o apsnd) (Logic.close_term params) binds;
- val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt;
- in (((vars', xs, params), propss, binds, binds'), params_ctxt) end;
+ val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
+ in ((vars' ~~ 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;
+val cert_statement = prep_statement cert_var cert_propp;
+val read_statement = prep_statement read_var read_propp;
end;