# HG changeset patch
# User wenzelm
# Date 1320683097 -3600
# Node ID 30f6617c9986f60313d1cc02187e96df6c8202c6
# Parent  ccffb3f9f42b5e096a823f88f7011c1ad1817702# Parent  e29521ef9059999f9ccb40daed3ccb655985f2b8
merged

diff -r ccffb3f9f42b -r 30f6617c9986 Admin/build
--- a/Admin/build	Mon Nov 07 14:16:01 2011 +0100
+++ b/Admin/build	Mon Nov 07 17:24:57 2011 +0100
@@ -84,7 +84,6 @@
 
 function build_jars ()
 {
-  "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
   popd >/dev/null
diff -r ccffb3f9f42b -r 30f6617c9986 NEWS
--- a/NEWS	Mon Nov 07 14:16:01 2011 +0100
+++ b/NEWS	Mon Nov 07 17:24:57 2011 +0100
@@ -10,22 +10,27 @@
 instead.  INCOMPATIBILITY.
 
 * Ancient code generator for SML and its commands 'code_module',
- 'code_library', 'consts_code', 'types_code' have been discontinued.
-  Use commands of the generic code generator instead. INCOMPATIBILITY.
-
-* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
-instead. INCOMPATIBILITY.
+'code_library', 'consts_code', 'types_code' have been discontinued.
+Use commands of the generic code generator instead. INCOMPATIBILITY.
+
+* Redundant attribute 'code_inline' has been discontinued. Use
+'code_unfold' instead. INCOMPATIBILITY.
+
 
 *** HOL ***
 
-* 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
-
-* 'Set.not_member' now qualifed.  INCOMPATIBILITY.
-
-* 'sublists' moved to More_List.thy.  INCOMPATIBILITY.
+* Clarified attribute "mono_set": pure declararation without modifying
+the result of the fact expression.
+
+* "Transitive_Closure.ntrancl": bounded transitive closure on
+relations.
+
+* Constant "Set.not_member" now qualifed.  INCOMPATIBILITY.
+
+* "sublists" moved to theory More_List.  INCOMPATIBILITY.
 
 * Theory Int: Discontinued many legacy theorems specific to type int.
-  INCOMPATIBILITY, use the corresponding generic theorems instead.
+INCOMPATIBILITY, use the corresponding generic theorems instead.
 
   zminus_zminus ~> minus_minus
   zminus_0 ~> minus_zero
@@ -62,17 +67,18 @@
   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
   zero_le_zpower_abs ~> zero_le_power_abs
 
-* New case_product attribute to generate a case rule doing multiple case
-  distinctions at the same time: E.g.
-
-    list.exhaust[case_product nat.exhaust]
-
-  produces a rule which can be used to perform case distinction on both
-  a list and a nat.
+* New "case_product" attribute to generate a case rule doing multiple
+case distinctions at the same time.  E.g.
+
+  list.exhaust [case_product nat.exhaust]
+
+produces a rule which can be used to perform case distinction on both
+a list and a nat.
+
 
 *** FOL ***
 
-* New case_product attribute (see HOL).
+* New "case_product" attribute (see HOL).
 
 
 *** ML ***
diff -r ccffb3f9f42b -r 30f6617c9986 lib/Tools/java
--- a/lib/Tools/java	Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/java	Mon Nov 07 17:24:57 2011 +0100
@@ -22,5 +22,5 @@
 fi
 
 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
 
diff -r ccffb3f9f42b -r 30f6617c9986 lib/Tools/scala
--- a/lib/Tools/scala	Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/scala	Mon Nov 07 17:24:57 2011 +0100
@@ -10,4 +10,4 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
diff -r ccffb3f9f42b -r 30f6617c9986 lib/Tools/scalac
--- a/lib/Tools/scalac	Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/scalac	Mon Nov 07 17:24:57 2011 +0100
@@ -10,4 +10,4 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
diff -r ccffb3f9f42b -r 30f6617c9986 lib/scripts/java_ext_dirs
--- a/lib/scripts/java_ext_dirs	Mon Nov 07 14:16:01 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Augment Java extension directories.
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## dependencies
-
-SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
-
-TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/java_ext_dirs.jar"
-
-if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
-  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
-  pushd "$TARGET_DIR" >/dev/null
-
-  BUILD="build$$"
-  TMP_JAR="java_ext_dirs$$.jar"
-
-  rm -rf "$BUILD" && mkdir "$BUILD"
-  javac -d "$BUILD" -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
-  jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce $TMP_JAR"
-  mv "$TMP_JAR" "$TARGET"
-  rm -rf "$BUILD"
-
-  popd >/dev/null
-fi
-
-
-## main
-
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
-  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
-
diff -r ccffb3f9f42b -r 30f6617c9986 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 17:24:57 2011 +0100
@@ -246,21 +246,19 @@
   shows "abelian_subgroup H G"
 proof -
   interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  by (rule a_comm_group)
+    by (rule a_comm_group)
   interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  by (rule a_subgroup)
+    by (rule a_subgroup)
 
   show "abelian_subgroup H G"
-  apply unfold_locales
+    apply unfold_locales
   proof (simp add: r_coset_def l_coset_def, clarsimp)
     fix x
     assume xcarr: "x \<in> carrier G"
-    from a_subgroup
-        have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
-    from xcarr Hcarr
-        show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
-        using m_comm[simplified]
-        by fast
+    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
+      unfolding subgroup_def by simp
+    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
+      using m_comm [simplified] by fast
   qed
 qed
 
@@ -543,9 +541,10 @@
 proof -
   interpret G: abelian_group G by fact
   interpret H: abelian_group H by fact
-  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
-    apply fact
-    apply fact
+  show ?thesis
+    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+      apply fact
+     apply fact
     apply (rule a_group_hom)
     done
 qed
diff -r ccffb3f9f42b -r 30f6617c9986 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -22,6 +22,8 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> Inductive.inductive_result * local_theory
+  val mono_add: attribute
+  val mono_del: attribute
   val codegen_preproc: theory -> thm list -> thm list
   val setup: theory -> theory
 end;
@@ -536,13 +538,12 @@
 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
 val add_inductive = Inductive.gen_add_inductive add_ind_set_def;
 
-fun mono_att att =  (* FIXME really mixed_attribute!? *)
-  Thm.mixed_attribute (fn (context, thm) =>
-    let val thm' = to_pred [] context thm
-    in (Thm.attribute_declaration att thm' context, thm') end);
+fun mono_att att =
+  Thm.declaration_attribute (fn thm => fn context =>
+    Thm.attribute_declaration att (to_pred [] context thm) context);
 
-val mono_add_att = mono_att Inductive.mono_add;
-val mono_del_att = mono_att Inductive.mono_del;
+val mono_add = mono_att Inductive.mono_add;
+val mono_del = mono_att Inductive.mono_del;
 
 
 (** package setup **)
@@ -556,7 +557,7 @@
     "convert rule to set notation" #>
   Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
     "convert rule to predicate notation" #>
-  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
     "declaration of monotonicity rule for set operators" #>
   Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
 
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -16,12 +16,12 @@
   val defined: theory -> string -> bool
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
-  val map_specs: ('a -> 'att) ->
+  val map_specs: ('a list -> 'att list) ->
     (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
-  val map_facts: ('a -> 'att) ->
+  val map_facts: ('a list -> 'att list) ->
     (('c * 'a list) * ('d * 'a list) list) list ->
     (('c * 'att list) * ('d * 'att list) list) list
-  val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
+  val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
@@ -127,9 +127,9 @@
 
 (* attributed declarations *)
 
-fun map_specs f = map (apfst (apsnd (map f)));
+fun map_specs f = map (apfst (apsnd f));
 
-fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
@@ -137,7 +137,7 @@
 
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
-    (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
+    (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
       [((Binding.empty, []), srcs)])
   |> fst |> maps snd;
 
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/element.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -481,7 +481,8 @@
 
 fun generic_note_thmss kind facts context =
   let
-    val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+    val facts' =
+      Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
   in
     context |> Context.mapping_result
       (Global_Theory.note_thmss kind facts')
@@ -492,14 +493,16 @@
   | init (Constrains _) = I
   | init (Assumes asms) = Context.map_proof (fn ctxt =>
       let
-        val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms;
+        val asms' =
+          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
         val (_, ctxt') = ctxt
           |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
           |> Proof_Context.add_assms_i Assumption.assume_export asms';
       in ctxt' end)
   | init (Defines defs) = Context.map_proof (fn ctxt =>
       let
-        val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs;
+        val defs' =
+          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
             in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -156,7 +156,7 @@
   in
     lthy
     |> target_notes kind global_facts local_facts
-    |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
+    |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
   end;
 
 
@@ -212,7 +212,7 @@
 fun theory_notes kind global_facts lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
+    val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
   in
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -562,8 +562,9 @@
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
             let
-              val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
-                Attrib.map_facts (Attrib.attribute_i thy)
+              val args'' = snd args'
+                |> Element.facts_map (Element.transform_ctxt morph)
+                |> Attrib.map_facts (map (Attrib.attribute_i thy));
             in Global_Theory.note_thmss kind args'' #> snd end)
         (registrations_of (Context.Theory thy) loc) thy))
   in ctxt'' end;
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -117,7 +117,7 @@
 
 fun locale_notes locale kind global_facts local_facts lthy =
   let
-    val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
+    val global_facts' = Attrib.map_facts (K []) global_facts;
     val local_facts' = Element.facts_map
       (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
   in
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/obtain.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -126,7 +126,7 @@
     val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
     val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
     val asm_props = maps (map fst) proppss;
-    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
+    val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
 
     (*obtain parms*)
     val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -593,7 +593,7 @@
 fun gen_assume asm prep_att exp args state =
   state
   |> assert_forward
-  |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args))
+  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
   |> these_factss [] |> #2;
 
 in
@@ -665,7 +665,9 @@
   state
   |> assert_forward
   |> map_context_result (Proof_Context.note_thmss ""
-    (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
+    (Attrib.map_facts_refs
+      (map (prep_atts (theory_of state)))
+      (prep_fact (context_of state)) args))
   |> these_factss (more_facts state)
   ||> opt_chain
   |> opt_result;
@@ -690,12 +692,12 @@
 
 local
 
-fun gen_using f g prep_atts prep_fact args state =
+fun gen_using f g prep_att prep_fact args state =
   state
   |> assert_backward
   |> map_context_result
     (Proof_Context.note_thmss ""
-      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+      (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
         (no_binding args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
@@ -916,7 +918,7 @@
   let
     val thy = theory_of state;
     val ((names, attss), propp) =
-      Attrib.map_specs (prep_att thy) stmt |> split_list |>> split_list;
+      Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
 
     fun after_qed' results =
       local_results ((names ~~ attss) ~~ results)
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -307,7 +307,7 @@
       let
         val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
-        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
+        val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
         val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
       in ((prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -231,48 +231,24 @@
 
 (* indexed syntax *)
 
+fun indexdefault_ast_tr [] =
+      Ast.Appl [Ast.Constant "_index",
+        Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
+  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
+
+fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]
+  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
+
 fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
 
-fun index_ast_tr ast =
-  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
-
-fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
-  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
-
-fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
-  | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
-
-fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
-  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
-
 fun index_tr [t] = t
   | index_tr ts = raise TERM ("index_tr", ts);
 
-
-(* implicit structures *)
-
-fun the_struct structs i =
-  if 1 <= i andalso i <= length structs then nth structs (i - 1)
-  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
+fun the_struct [] = error "Illegal reference to implicit structure"
+  | the_struct (x :: _) = x;
 
-fun legacy_struct structs i =
-  let
-    val x = the_struct structs i;
-    val _ =
-      legacy_feature
-        ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
-          Position.str_of (Position.thread_data ()) ^
-          " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
-          (if i = 1 then " (may be omitted)" else ""))
-  in x end;
-
-fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
-  | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
-  | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      (case Lexicon.read_nat s of
-        SOME i => Syntax.free (legacy_struct structs i)
-      | NONE => raise TERM ("struct_tr", [t]))
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs)
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
@@ -517,17 +493,9 @@
 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   | index_ast_tr' _ = raise Match;
 
-
-(* implicit structures *)
-
-fun the_struct' structs s =
-  [(case Lexicon.read_nat s of
-    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
-  | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
-
-fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
-  | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
-      the_struct' structs s
+fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =
+      Ast.Appl [Ast.Constant "_free",
+        Ast.Variable (the_struct structs handle ERROR _ => raise Match)]
   | struct_ast_tr' _ _ = raise Match;
 
 
@@ -547,7 +515,6 @@
     ("_idtypdummy", idtypdummy_ast_tr),
     ("_bigimpl", bigimpl_ast_tr),
     ("_indexdefault", indexdefault_ast_tr),
-    ("_indexnum", indexnum_ast_tr),
     ("_indexvar", indexvar_ast_tr),
     ("_struct", struct_ast_tr)],
    [("_abs", abs_tr),
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/System/Java_Ext_Dirs.java
--- a/src/Pure/System/Java_Ext_Dirs.java	Mon Nov 07 14:16:01 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-/*  Title:      Pure/System/Java_Ext_Dirs.java
-    Author:     Makarius
-
-Augment Java extension directories.
-*/
-
-package isabelle;
-
-public class Java_Ext_Dirs
-{
-  public static void main(String [] args) {
-    StringBuilder s = new StringBuilder();
-    int i;
-    for (i = 0; i < args.length; i++) {
-      s.append(args[i]);
-      s.append(System.getProperty("path.separator"));
-    }
-    s.append(System.getProperty("java.ext.dirs"));
-    System.out.println(s.toString());
-  }
-}
-
diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 07 17:24:57 2011 +0100
@@ -127,8 +127,6 @@
     ("_strip_positions", typ "'a", NoSyn),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
-    ("_index1",     typ "index",                       Delimfix "\\<^sub>1"),
-    ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
diff -r ccffb3f9f42b -r 30f6617c9986 src/Tools/JVM/Java_Ext_Dirs.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/Java_Ext_Dirs.java	Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,22 @@
+/*  Title:      Pure/System/Java_Ext_Dirs.java
+    Author:     Makarius
+
+Augment Java extension directories.
+*/
+
+package isabelle;
+
+public class Java_Ext_Dirs
+{
+  public static void main(String [] args) {
+    StringBuilder s = new StringBuilder();
+    int i;
+    for (i = 0; i < args.length; i++) {
+      s.append(args[i]);
+      s.append(System.getProperty("path.separator"));
+    }
+    s.append(System.getProperty("java.ext.dirs"));
+    System.out.println(s.toString());
+  }
+}
+
diff -r ccffb3f9f42b -r 30f6617c9986 src/Tools/JVM/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/build	Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Offline build script for JVM tools.
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## build
+
+cd "$(dirname "$0")"
+
+SOURCE="Java_Ext_Dirs.java"
+TARGET="java_ext_dirs.jar"
+
+BUILD="build_dir$$"
+TMP_JAR="java_ext_dirs$$.jar"
+
+rm -rf "$BUILD" && mkdir "$BUILD"
+javac -source 1.4 -target 1.4 -d "$BUILD" "$SOURCE" || fail "Failed to compile sources"
+jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce \"$TMP_JAR\""
+mv "$TMP_JAR" "$TARGET"
+rm -rf "$BUILD"
+
diff -r ccffb3f9f42b -r 30f6617c9986 src/Tools/JVM/java_ext_dirs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/java_ext_dirs	Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Augment Java extension directories.
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
+  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+
diff -r ccffb3f9f42b -r 30f6617c9986 src/Tools/JVM/java_ext_dirs.jar
Binary file src/Tools/JVM/java_ext_dirs.jar has changed