# HG changeset patch
# User wenzelm
# Date 1190838062 -7200
# Node ID ff617b6711f42d1c8760924663cfe4ba94bfc770
# Parent  59e0b49688fb0c2083af1a35f0e4a41d7a0e9155
read/check_specification: free_dummy_patterns;

diff -r 59e0b49688fb -r ff617b6711f4 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Sep 26 22:20:59 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Sep 26 22:21:02 2007 +0200
@@ -116,11 +116,15 @@
     val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
 
     val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
-    val idx = (fold o fold o fold) Term.maxidx_term Asss ~1 + 1;
+    val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
+      |> 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)
+        #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 specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;