clarified modules;

--- a/src/Pure/Isar/obtain.ML	Fri Apr 22 15:34:37 2016 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Apr 24 20:29:49 2016 +0200
@@ -193,47 +193,28 @@
 
 local
 
-fun gen_obtain prep_att prep_var prep_propp
-    that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state =
   let
     val _ = Proof.assert_forward_or_chain state;
-    val ctxt = Proof.context_of state;
 
-    (*vars*)
-    val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
-    val ((xs', vars), fix_ctxt) = thesis_ctxt
-      |> fold_map prep_var raw_vars
-      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
-    val xs = map (Variable.check_name o #1) vars;
+    val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
 
-    (*asms*)
-    val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
-    val props = flat propss;
-    val declare_asms =
-      fold Variable.declare_term props #>
-      fold Variable.bind_term binds;
+    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 asms =
-      map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
+      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
       map (map (rpair [])) propss;
 
-    (*params*)
-    val (params, params_ctxt) =
-      declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
-    val cparams = map (Thm.cterm_of params_ctxt) params;
-    val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
-
-    val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-
-    (*statements*)
     val that_prop =
       Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
+        (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.map_context declare_asms
+        |> Proof.map_context (fold Variable.bind_term binds)
         |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
       end;
   in
@@ -248,8 +229,8 @@
 
 in
 
-val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp;
+val obtain = gen_obtain Proof_Context.cert_spec (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd;
 
 end;
 

--- 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 **)