# HG changeset patch
# User wenzelm
# Date 1434206127 -7200
# Node ID a4c6b278f3a7edeeb3a4bd55d95efc727ab89391
# Parent  ba9085f7433ff059205787a9ba80c7de24aaa387
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

diff -r ba9085f7433f -r a4c6b278f3a7 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jun 13 16:35:27 2015 +0200
@@ -33,8 +33,6 @@
   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) ->
@@ -250,26 +248,6 @@
 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 **)
 
diff -r ba9085f7433f -r a4c6b278f3a7 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Jun 13 16:35:27 2015 +0200
@@ -96,12 +96,9 @@
   let
     val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
     val xs = map (Variable.check_name o #1) vars;
-
-    val default_name = AList.lookup (op =) (xs' ~~ xs);
-    val default_type = Variable.default_type ctxt';
   in
     Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
-    |> Element.close_form ctxt default_name default_type
+    |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
   end;
 
 fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
diff -r ba9085f7433f -r a4c6b278f3a7 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Jun 13 16:35:27 2015 +0200
@@ -105,11 +105,12 @@
 
 fun close_forms ctxt i As =
   let
-    val frees = rev (fold (Variable.add_free_names ctxt) As []);
+    val xs = rev (fold (Variable.add_free_names ctxt) As []);
     val types =
-      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
-    val uniform_typing = AList.lookup (op =) (frees ~~ types);
-  in map (Element.close_form ctxt (K NONE) uniform_typing) As end;
+      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
+    val uniform_typing = AList.lookup (op =) (xs ~~ types);
+    val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
+  in map close As end;
 
 fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
diff -r ba9085f7433f -r a4c6b278f3a7 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/logic.ML	Sat Jun 13 16:35:27 2015 +0200
@@ -12,6 +12,8 @@
   val is_all: term -> bool
   val dest_all: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
+  val all_constraint: (string -> typ option) -> string * string -> term -> term
+  val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
   val mk_equals: term * term -> term
   val dest_equals: term -> term * term
   val implies: term
@@ -109,6 +111,35 @@
   | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
 
 
+(* operations before type-inference *)
+
+local
+
+fun abs_body default_type z tm =
+  let
+    fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
+      | abs lev (t $ u) = abs lev t $ abs lev u
+      | abs lev (a as Free (x, T)) =
+          if x = z then
+            Type.constraint (the_default dummyT (default_type x))
+              (Type.constraint T (Bound lev))
+          else a
+      | abs _ a = a;
+  in abs 0 (Term.incr_boundvars 1 tm) end;
+
+in
+
+fun all_constraint default_type (y, z) t =
+  all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
+
+fun dependent_all_constraint default_type (y, z) t =
+  let val t' = abs_body default_type z t
+  in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
+
+end;
+
+
+
 (** equality **)
 
 fun mk_equals (t, u) =