# HG changeset patch
# User wenzelm
# Date 1138727976 -3600
# Node ID b8a1c3cdf739b4b9bb141a5c56c9f9998f431ec7
# Parent  7aa8cd3812d3b2e19dc0fb6a642309b03273010c
axiomatization: retrict parameters to occurrences in specs;
definition: restrict parameters to individual rhs;

diff -r 7aa8cd3812d3 -r b8a1c3cdf739 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Jan 31 18:19:35 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Jan 31 18:19:36 2006 +0100
@@ -70,22 +70,23 @@
     val ctxt = init context;
     val (vars, specs) = fst (prep raw_vars raw_specs ctxt);
     val cs = map fst vars;
+    val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []);
 
-    val (consts, consts_ctxt) = ctxt |> LocalTheory.consts vars;
+    val (consts, consts_ctxt) = ctxt |> LocalTheory.consts_restricted spec_frees vars;
     val subst = Term.subst_atomic (map Free cs ~~ consts);
 
     val (axioms, axioms_ctxt) =
       consts_ctxt
       |> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props)))
       ||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts));
-    val _ = print ctxt cs;
+    val _ = print ctxt spec_frees cs;
   in ((consts, axioms), exit axioms_ctxt) end;
 
 fun axiomatization loc =
   gen_axioms read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts;
 fun axiomatization_i loc =
   gen_axioms cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts;
-val axiomatization_loc = gen_axioms cert_specification I I (K (K ()));
+val axiomatization_loc = gen_axioms cert_specification I I (K (K (K ())));
 
 
 (* definition *)
@@ -107,13 +108,14 @@
 
     val ctxt = init context;
     val ((cs, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list;
-    val _ = print ctxt cs;
+    val def_frees = member (op =) (fold (Term.add_frees o fst) defs []);
+    val _ = print ctxt def_frees cs;
   in (defs, exit defs_ctxt) end;
 
 fun definition loc =
   gen_defs read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts;
 fun definition_i loc =
   gen_defs cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts;
-val definition_loc = gen_defs cert_specification I I (K (K ()));
+val definition_loc = gen_defs cert_specification I I (K (K (K ())));
 
 end;