# HG changeset patch
# User wenzelm
# Date 1461744215 -7200
# Node ID c9605a284fbad83283503938281ec45a159e3fc5
# Parent  60406bf310f8e9598bb08638d941a97036f5ecf3
tuned;

diff -r 60406bf310f8 -r c9605a284fba src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Apr 26 22:59:25 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 27 10:03:35 2016 +0200
@@ -105,14 +105,15 @@
 
 local
 
-fun close_forms ctxt i As =
+fun close_forms ctxt auto_close i prems concls =
   let
-    val xs = rev (fold (Variable.add_free_names ctxt) As []);
+    val xs =
+      if auto_close then rev (fold (Variable.add_free_names ctxt) (concls @ prems) [])
+      else [];
     val types =
       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;
+  in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
 
 fun get_positions ctxt x =
   let
@@ -127,7 +128,7 @@
       | get _ _ = [];
   in get [] end;
 
-fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
   let
     val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
     val (xs, params_ctxt) = vars_ctxt
@@ -139,20 +140,21 @@
         (map (Binding.pos_of o #1) vars ~~
           map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
 
-    val Asss =
+    val Asss0 =
       (map o map) snd raw_specss
       |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
-    val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
+    val names =
+      Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
       |> fold Name.declare xs;
-    val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
-    val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1;
 
-    val specs =
-      (if do_close then
-        #1 (fold_map
-            (fn Ass => fn i => (burrow (close_forms params_ctxt i) Ass, i + 1)) Asss' idx)
-      else Asss')
-      |> flat |> burrow (Syntax.check_props params_ctxt);
+    val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names;
+    val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
+
+    val (Asss2, _) =
+      fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt auto_close i []) Ass, i + 1))
+        Asss1 idx;
+
+    val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
     val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
 
     val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
@@ -161,19 +163,17 @@
       map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
 
     fun get_pos x =
-      if do_close then Position.none
-      else
-        (case (maps o maps o maps) (get_positions specs_ctxt x) Asss' of
-          [] => Position.none
-        | pos :: _ => pos);
+      (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
+        [] => Position.none
+      | pos :: _ => pos);
   in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
 
 
 fun single_spec (a, prop) = [(a, [prop])];
 fun the_spec (a, [prop]) = (a, prop);
 
-fun prep_spec prep_var parse_prop prep_att do_close vars specs =
-  prepare prep_var parse_prop prep_att do_close
+fun prep_spec prep_var parse_prop prep_att auto_close vars specs =
+  prepare prep_var parse_prop prep_att auto_close
     vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
 
 in
diff -r 60406bf310f8 -r c9605a284fba src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Apr 26 22:59:25 2016 +0200
+++ b/src/Pure/logic.ML	Wed Apr 27 10:03:35 2016 +0200
@@ -28,6 +28,8 @@
   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 close_prop_constraint: (string -> typ option) ->
+    (string * string) list -> term list -> term -> term
   val true_prop: term
   val conjunction: term
   val mk_conjunction: term * term -> term
@@ -205,10 +207,15 @@
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 
-(* close *)
+(* close -- omit vacuous quantifiers *)
 
 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));
+
+fun close_prop xs As B =
+  fold_rev dependent_all_name xs (list_implies (As, B));
+
+fun close_prop_constraint default_type xs As B =
+  fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B));
 
 
 (** conjunction **)