src/Pure/Isar/element.ML

   val transform_ctxt: morphism -> context_i -> context_i
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_ctxt_no_attribs: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
+  val close_form: Proof.context -> (string -> string option) -> (string -> typ option) ->
+    term -> term
   type witness
   val prove_witness: Proof.context -> term -> tactic -> witness
   val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
     term list list -> Proof.context -> Proof.state
   val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->

   end |> thm_name kind raw_th;
 
 end;
 
 
+(** abstract syntax operations: before type-inference **)
+
+fun close_form ctxt default_name default_type A =
+  let
+    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
+      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
+      | abs_body lev y (t as Free (x, T)) =
+          if x = y then
+            Type.constraint (the_default dummyT (default_type x))
+              (Type.constraint T (Bound lev))
+          else t
+      | abs_body _ _ a = a;
+    fun close y B =
+      let
+        val y' = perhaps default_name y;
+        val B' = abs_body 0 y (Term.incr_boundvars 1 B);
+      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y', dummyT, B') else B end;
+  in fold close (Variable.add_free_names ctxt A []) A end;
+
+
 
 (** logical operations **)
 
 (* witnesses -- hypotheses as protected facts *)