# 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;