# HG changeset patch
# User wenzelm
# Date 1121786505 -7200
# Node ID 3057990d20e07ae78199218e0a904d597b1ea554
# Parent  9ed940a1bebb71464bfe80866a52681300444c5b
tuned;

diff -r 9ed940a1bebb -r 3057990d20e0 bin/isabelle-process
--- a/bin/isabelle-process	Tue Jul 19 16:16:53 2005 +0200
+++ b/bin/isabelle-process	Tue Jul 19 17:21:45 2005 +0200
@@ -198,9 +198,10 @@
 ## prepare tmp directory
 
 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+ISABELLE_PID="$$"
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX${ISABELLE_PID}"
+mkdir -p "$ISABELLE_TMP"
 
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
-mkdir -p "$ISABELLE_TMP"
 
 ## run it!
 
@@ -216,8 +217,8 @@
   MLTEXT="$MLTEXT; Isar.main();"
 fi
 
-export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
-export ISABELLE_PID="$$"
+export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
+  ISABELLE_PID ISABELLE_TMP
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
diff -r 9ed940a1bebb -r 3057990d20e0 lib/Tools/latex
--- a/lib/Tools/latex	Tue Jul 19 16:16:53 2005 +0200
+++ b/lib/Tools/latex	Tue Jul 19 17:21:45 2005 +0200
@@ -85,11 +85,8 @@
 {
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
   do
-    TARGET="$DIR"/$(basename $STYLEFILE)
-    rm -f $TARGET
-    "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g; print;' "$STYLEFILE" > "$TARGET"
-    #~ "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET
-    # the [I] is there to prevent CVS from expanding $Id...$ itself ;-)
+    TARGET="$DIR"/$(basename "$STYLEFILE")
+    "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
   done
 }
 
diff -r 9ed940a1bebb -r 3057990d20e0 src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Tue Jul 19 16:16:53 2005 +0200
+++ b/src/Pure/fact_index.ML	Tue Jul 19 17:21:45 2005 +0200
@@ -25,20 +25,20 @@
 
 (* indexing items *)
 
-fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
-  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
-  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
-  | add_frees _ (_, xs) = xs;
+val add_consts = fold_aterms
+  (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
 
-fun index_term pred t (cs, xs) =
-  (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
+fun add_frees pred = fold_aterms
+  (fn Free (x, _) => if pred x then insert (op =) x else I | _ => I);
+
+fun index_term pred t (cs, xs) = (add_consts t cs, add_frees pred t xs);
 
 fun index_thm pred th idx =
   let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
     idx
     |> index_term pred prop
     |> fold (index_term pred) hyps
-    |> fold (index_term pred) (Thm.terms_of_tpairs tpairs)
+    |> fold (fn (t, u) => index_term pred t #> index_term pred u) tpairs
   end;