# HG changeset patch
# User wenzelm
# Date 1461680428 -7200
# Node ID 9b95ae9ec6719d98b9cf7c36e843b362ebc56ee3
# Parent  ae0ca486bd3fe3d737d8e77a741d84b9071c9401
defs are closed, which leads to proper auto_bind_facts;
misc tuning;

diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 16:20:28 2016 +0200
@@ -193,27 +193,27 @@
 
 local
 
-fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_statement prep_att that_binding raw_vars raw_asms int state =
   let
     val _ = Proof.assert_forward_or_chain state;
 
     val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
+    val ((vars, propss, binds, binds'), params_ctxt) =
+      prep_statement raw_vars (map #2 raw_asms) thesis_ctxt;
+    val params = map #2 vars;
+    val that_prop =
+      Logic.list_rename_params (map #1 params)
+        (fold_rev Logic.all (map #2 params) (Logic.list_implies (flat propss, thesis)));
 
-    val (((vars, xs, params), propss, binds, binds'), params_ctxt) =
-      prep_spec raw_vars (map #2 raw_asms) thesis_ctxt;
-    val cparams = map (Thm.cterm_of params_ctxt) params;
+    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) vars;
     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
       map (map (rpair [])) propss;
 
-    val that_prop =
-      Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (flat propss, thesis)));
-
     fun after_qed (result_ctxt, results) state' =
       let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
         state'
-        |> Proof.fix vars
+        |> Proof.fix (map #1 vars)
         |> Proof.map_context (fold Variable.bind_term binds)
         |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
       end;
@@ -229,8 +229,8 @@
 
 in
 
-val obtain = gen_obtain Proof_Context.cert_spec (K I);
-val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd;
+val obtain = gen_obtain Proof_Context.cert_statement (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_statement Attrib.attribute_cmd;
 
 end;
 
diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 26 16:20:28 2016 +0200
@@ -694,13 +694,9 @@
     val ctxt = context_of state;
 
     val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
-    val (params, prems_propss, concl_propss, result_binds) =
-      #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
-
-    fun close prop =
-      fold_rev Logic.dependent_all_name params
-        (Logic.list_implies (flat prems_propss, prop));
-    val propss = (map o map) close concl_propss;
+    val ((params, prems_propss, concl_propss, result_binds), _) =
+      prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt;
+    val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
   in
     state
     |> assert_forward
@@ -893,45 +889,37 @@
 
 local
 
-fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
-      if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
-      else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
-  | match_defs [] [] = []
-  | match_defs more_decls more_defs =
-      error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
-        (if null more_decls then "" else " ") ^
-        "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
-
-fun invisible_fixes vars ctxt = ctxt
-  |> Context_Position.set_visible false
-  |> Proof_Context.add_fixes vars |> #2
-  |> Context_Position.restore_visible ctxt;
-
-fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
+fun gen_define prep_statement prep_att raw_decls raw_fixes raw_defs state =
   let
     val _ = assert_forward state;
     val ctxt = context_of state;
 
     (*vars*)
-    val n_vars = length raw_vars;
-    val (((all_vars, _, all_params), defss, _, binds'), _) =
-      prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
-    val (vars, fixes) = chop n_vars all_vars;
-    val (params, _) = chop n_vars all_params;
+    val ((vars, propss, _, binds'), vars_ctxt) =
+      prep_statement (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
+    val (decls, fixes) = chop (length raw_decls) vars;
+    val show_term = Syntax.string_of_term vars_ctxt;
 
     (*defs*)
-    val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
-    val defs1 = map derived_def (flat defss);
-    val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
+    fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
+          if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+          else
+            error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
+              show_term (Free (y, U)))
+      | match_defs [] [] = []
+      | match_defs more_decls more_defs =
+          error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^
+            (if null more_decls then "" else " ") ^
+            "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
+
+    val derived_def = Local_Defs.derived_def ctxt {conditional = false};
+    val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
+    val defs2 = match_defs decls defs1;
     val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
 
-    (*fixes*)
-    val fixes_ctxt = invisible_fixes fixes defs_ctxt;
-    val export = singleton (Variable.export fixes_ctxt defs_ctxt);
-
     (*notes*)
     val def_thmss =
-      map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
+      map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th))
         (defs1 ~~ defs2 ~~ defs3)
       |> unflat (map snd raw_defs);
     val notes =
@@ -947,8 +935,8 @@
 
 in
 
-val define = gen_define Proof_Context.cert_spec (K I);
-val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
+val define = gen_define Proof_Context.cert_statement (K I);
+val define_cmd = gen_define Proof_Context.read_statement Attrib.attribute_cmd;
 
 end;
 
diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/proof_context.ML
--- 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;
 
diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/logic.ML	Tue Apr 26 16:20:28 2016 +0200
@@ -26,6 +26,8 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val nth_prem: int * term -> term
+  val close_term: (string * term) list -> term -> term
+  val close_prop: (string * term) list -> term list -> term -> term
   val true_prop: term
   val conjunction: term
   val mk_conjunction: term * term -> term
@@ -147,7 +149,6 @@
 end;
 
 
-
 (** equality **)
 
 fun mk_equals (t, u) =
@@ -204,6 +205,11 @@
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 
+(* close *)
+
+val close_term = fold_rev Term.dependent_lambda_name;
+fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B));
+
 
 (** conjunction **)