# HG changeset patch
# User wenzelm
# Date 1434013745 -7200
# Node ID 1338e6b4395214f09b62c6c47836d41d1c4eb98d
# Parent  9945378d1ee799392163f67dc6193979207cd373
tuned -- eliminated unused feature;

diff -r 9945378d1ee7 -r 1338e6b43952 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Jun 11 10:44:04 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Jun 11 11:09:05 2015 +0200
@@ -103,13 +103,9 @@
 
 local
 
-fun close_forms ctxt i xs As =
+fun close_forms ctxt i As =
   let
-    val commons = map #1 xs;
-    val _ =
-      (case duplicates (op =) commons of [] => ()
-      | dups => error ("Duplicate local variables " ^ commas_quote dups));
-    val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
+    val frees = 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 = the o AList.lookup (op =) (frees ~~ types);
@@ -120,14 +116,10 @@
           if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
           else t
       | abs_body _ _ a = a;
-    fun close (y, U) B =
+    fun close y B =
       let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
-      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
-    fun close_form A =
-      let
-        val occ_frees = rev (Variable.add_free_names ctxt A []);
-        val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
-      in fold_rev close bounds A end;
+      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, dummyT, B') else B end;
+    fun close_form A = fold close (Variable.add_free_names ctxt A []) A;
   in map close_form As end;
 
 fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
@@ -145,7 +137,7 @@
     val specs =
       (if do_close then
         #1 (fold_map
-            (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx)
+            (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 specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;