merged
authorhaftmann
Mon, 20 Dec 2010 17:31:58 +0100
changeset 41312 054a4e5ac5fb
parent 41310 65631ca437c9 (diff)
parent 41311 de0c906dfe60 (current diff)
child 41319 33e107788595
merged
--- a/NEWS	Mon Dec 20 15:37:25 2010 +0100
+++ b/NEWS	Mon Dec 20 17:31:58 2010 +0100
@@ -603,7 +603,9 @@
 
 *** FOL and ZF ***
 
-* All constant names are now qualified.  INCOMPATIBILITY.
+* All constant names are now qualified internally and use proper
+identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
+
 
 
 *** ML ***
--- a/src/CTT/CTT.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/CTT/CTT.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -54,7 +54,7 @@
   lambda    :: "(i => i) => i"      (binder "lam " 10)
   app       :: "[i,i]=>i"           (infixl "`" 60)
   (*Natural numbers*)
-  "0"       :: "i"                  ("0")
+  Zero      :: "i"                  ("0")
   (*Pairing*)
   pair      :: "[i,i]=>i"           ("(1<_,/_>)")
 
--- a/src/FOL/FOL.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/FOL.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -175,7 +175,7 @@
   (
     val thy = @{theory}
     type claset = Cla.claset
-    val equality_name = @{const_name "op ="}
+    val equality_name = @{const_name eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
@@ -391,4 +391,7 @@
 setup Induct.setup
 declare case_split [cases type: o]
 
+
+hide_const (open) eq
+
 end
--- a/src/FOL/IFOL.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/IFOL.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -42,13 +42,13 @@
 
   (* Connectives *)
 
-  "op ="        :: "['a, 'a] => o"              (infixl "=" 50)
+  eq            :: "['a, 'a] => o"              (infixl "=" 50)
 
   Not           :: "o => o"                     ("~ _" [40] 40)
-  "op &"        :: "[o, o] => o"                (infixr "&" 35)
-  "op |"        :: "[o, o] => o"                (infixr "|" 30)
-  "op -->"      :: "[o, o] => o"                (infixr "-->" 25)
-  "op <->"      :: "[o, o] => o"                (infixr "<->" 25)
+  conj          :: "[o, o] => o"                (infixr "&" 35)
+  disj          :: "[o, o] => o"                (infixr "|" 30)
+  imp           :: "[o, o] => o"                (infixr "-->" 25)
+  iff           :: "[o, o] => o"                (infixr "<->" 25)
 
   (* Quantifiers *)
 
@@ -69,28 +69,24 @@
 
 notation (xsymbols)
   Not       ("\<not> _" [40] 40) and
-  "op &"    (infixr "\<and>" 35) and
-  "op |"    (infixr "\<or>" 30) and
+  conj      (infixr "\<and>" 35) and
+  disj      (infixr "\<or>" 30) and
   All       (binder "\<forall>" 10) and
   Ex        (binder "\<exists>" 10) and
   Ex1       (binder "\<exists>!" 10) and
-  "op -->"  (infixr "\<longrightarrow>" 25) and
-  "op <->"  (infixr "\<longleftrightarrow>" 25)
+  imp       (infixr "\<longrightarrow>" 25) and
+  iff       (infixr "\<longleftrightarrow>" 25)
 
 notation (HTML output)
   Not       ("\<not> _" [40] 40) and
-  "op &"    (infixr "\<and>" 35) and
-  "op |"    (infixr "\<or>" 30) and
+  conj      (infixr "\<and>" 35) and
+  disj      (infixr "\<or>" 30) and
   All       (binder "\<forall>" 10) and
   Ex        (binder "\<exists>" 10) and
   Ex1       (binder "\<exists>!" 10)
 
 finalconsts
-  False All Ex
-  "op ="
-  "op &"
-  "op |"
-  "op -->"
+  False All Ex eq conj disj imp
 
 axioms
 
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -156,7 +156,7 @@
     end;
 *}
 
-local_setup {* Config.put show_hyps true *}
+declare [[show_hyps]]
 
 ML {*
   check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
--- a/src/FOL/ex/Nat.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/Nat.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
 arities nat :: "term"
 
 consts
-  0 :: nat    ("0")
+  Zero :: nat    ("0")
   Suc :: "nat => nat"
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
   add :: "[nat, nat] => nat"    (infixl "+" 60)
--- a/src/FOL/ex/ROOT.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/ROOT.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -1,8 +1,3 @@
-(*  Title:      FOL/ex/ROOT.ML
-
-Examples for First-Order Logic. 
-*)
-
 use_thys [
   "First_Order_Logic",
   "Natural_Numbers",
@@ -21,5 +16,4 @@
   "If"
 ];
 
-(*regression test for locales -- sets several global flags!*)
 no_document use_thy "Locale_Test/Locale_Test";
--- a/src/FOL/fologic.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/fologic.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -50,29 +50,29 @@
 (* Logical constants *)
 
 val not = Const (@{const_name Not}, oT --> oT);
-val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
-val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
-val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
-val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
+val conj = Const(@{const_name conj}, [oT,oT]--->oT);
+val disj = Const(@{const_name disj}, [oT,oT]--->oT);
+val imp = Const(@{const_name imp}, [oT,oT]--->oT)
+val iff = Const(@{const_name iff}, [oT,oT]--->oT);
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
 and mk_imp (t1, t2) = imp $ t1 $ t2
 and mk_iff (t1, t2) = iff $ t1 $ t2;
 
-fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
-fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
-fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
   | dest_iff  t = raise TERM ("dest_iff", [t]);
 
-fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
+fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
-fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
--- a/src/FOL/simpdata.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/simpdata.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -8,15 +8,15 @@
 (*Make meta-equalities.  The operator below is Trueprop*)
 
 fun mk_meta_eq th = case concl_of th of
-    _ $ (Const(@{const_name "op ="},_)$_$_)   => th RS @{thm eq_reflection}
-  | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
+    _ $ (Const(@{const_name eq},_)$_$_)   => th RS @{thm eq_reflection}
+  | _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
   | _                           =>
   error("conclusion must be a =-equality or <->");;
 
 fun mk_eq th = case concl_of th of
     Const("==",_)$_$_           => th
-  | _ $ (Const(@{const_name "op ="},_)$_$_)   => mk_meta_eq th
-  | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+  | _ $ (Const(@{const_name eq},_)$_$_)   => mk_meta_eq th
+  | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
   | _ $ (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
   | _                           => th RS @{thm iff_reflection_T};
 
@@ -32,7 +32,7 @@
       error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 val mksimps_pairs =
-  [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+  [(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
    (@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
 
 fun mk_atomize pairs =
@@ -55,11 +55,11 @@
 structure Quantifier1 = Quantifier1Fun(
 struct
   (*abstract syntax*)
-  fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
+  fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
     | dest_eq _ = NONE;
-  fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
+  fun dest_conj((c as Const(@{const_name conj},_)) $ s $ t) = SOME(c,s,t)
     | dest_conj _ = NONE;
-  fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
+  fun dest_imp((c as Const(@{const_name imp},_)) $ s $ t) = SOME(c,s,t)
     | dest_imp _ = NONE;
   val conj = FOLogic.conj
   val imp  = FOLogic.imp
--- a/src/FOLP/IFOLP.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -24,14 +24,14 @@
  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
 
       (*** Logical Connectives -- Type Formers ***)
- "op ="         ::      "['a,'a] => o"  (infixl "=" 50)
+ eq             ::      "['a,'a] => o"  (infixl "=" 50)
  True           ::      "o"
  False          ::      "o"
  Not            ::      "o => o"        ("~ _" [40] 40)
- "op &"         ::      "[o,o] => o"    (infixr "&" 35)
- "op |"         ::      "[o,o] => o"    (infixr "|" 30)
- "op -->"       ::      "[o,o] => o"    (infixr "-->" 25)
- "op <->"       ::      "[o,o] => o"    (infixr "<->" 25)
+ conj           ::      "[o,o] => o"    (infixr "&" 35)
+ disj           ::      "[o,o] => o"    (infixr "|" 30)
+ imp            ::      "[o,o] => o"    (infixr "-->" 25)
+ iff            ::      "[o,o] => o"    (infixr "<->" 25)
       (*Quantifiers*)
  All            ::      "('a => o) => o"        (binder "ALL " 10)
  Ex             ::      "('a => o) => o"        (binder "EX " 10)
@@ -51,9 +51,9 @@
  inr            :: "p=>p"
  when           :: "[p, p=>p, p=>p]=>p"
  lambda         :: "(p => p) => p"      (binder "lam " 55)
- "op `"         :: "[p,p]=>p"           (infixl "`" 60)
+ App            :: "[p,p]=>p"           (infixl "`" 60)
  alll           :: "['a=>p]=>p"         (binder "all " 55)
- "op ^"         :: "[p,'a]=>p"          (infixl "^" 55)
+ app            :: "[p,'a]=>p"          (infixl "^" 55)
  exists         :: "['a,p]=>p"          ("(1[_,/_])")
  xsplit         :: "[p,['a,p]=>p]=>p"
  ideq           :: "'a=>p"
@@ -595,7 +595,7 @@
 struct
   (*Take apart an equality judgement; otherwise raise Match!*)
   fun dest_eq (Const (@{const_name Proof}, _) $
-    (Const (@{const_name "op ="}, _)  $ t $ u) $ _) = (t, u);
+    (Const (@{const_name eq}, _)  $ t $ u) $ _) = (t, u);
 
   val imp_intr = @{thm impI}
 
--- a/src/FOLP/ex/Nat.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/ex/Nat.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
 arities nat :: "term"
 
 consts
-  0 :: nat    ("0")
+  Zero :: nat    ("0")
   Suc :: "nat => nat"
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
   add :: "[nat, nat] => nat"    (infixl "+" 60)
--- a/src/FOLP/simpdata.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/simpdata.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -17,15 +17,15 @@
 (* Conversion into rewrite rules *)
 
 fun mk_eq th = case concl_of th of
-      _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
-    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+      _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+    | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
     | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
     | _ => make_iff_T th;
 
 
 val mksimps_pairs =
-  [(@{const_name "op -->"}, [@{thm mp}]),
-   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+  [(@{const_name imp}, [@{thm mp}]),
+   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
    (@{const_name "All"}, [@{thm spec}]),
    (@{const_name True}, []),
    (@{const_name False}, [])];
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
 
 consts
 
-  "{|}"  :: "'a multiset"                        ("{|}")
+  emptym :: "'a multiset"                        ("{|}")
   addm   :: "['a multiset, 'a] => 'a multiset"
   delm   :: "['a multiset, 'a] => 'a multiset"
   countm :: "['a multiset, 'a => bool] => nat"
--- a/src/HOL/Library/Sum_Of_Squares/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
 ISABELLE_SUM_OF_SQUARES="$COMPONENT"
--- a/src/HOL/Mirabelle/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mirabelle/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
 MIRABELLE_HOME="$COMPONENT"
 
 MIRABELLE_LOGIC=HOL
@@ -5,4 +7,4 @@
 MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
 MIRABELLE_TIMEOUT=30
 
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mutabelle/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,7 +1,9 @@
+# -*- shell-script -*- :mode=shellscript:
+
 MUTABELLE_HOME="$COMPONENT"
 
 DEFAULT_MUTABELLE_LOGIC=HOL
 DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main
 DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
 
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Dec 20 17:31:58 2010 +0100
@@ -2,7 +2,7 @@
 #
 # Author: Lukas Bulwahn
 #
-# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
+# DESCRIPTION: mutant-testing for counterexample generators and automated tools
 
 
 PRG="$(basename "$0")"
@@ -16,7 +16,8 @@
   echo "    -T THEORY    parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
   echo "    -O DIR       output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)"
   echo
-  echo "  THEORY is the name of the theory of which all theorems should be mutated and tested"
+  echo "  THEORY is the name of the theory of which all theorems should be"
+  echo "  mutated and tested."
   echo
   exit 1
 }
--- a/src/HOL/Prolog/Test.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Prolog/Test.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -37,9 +37,9 @@
   sue     :: person
   ned     :: person
 
-  "23"    :: nat          ("23")
-  "24"    :: nat          ("24")
-  "25"    :: nat          ("25")
+  nat23   :: nat          ("23")
+  nat24   :: nat          ("24")
+  nat25   :: nat          ("25")
 
   age     :: "[person, nat]                          => bool"
 
--- a/src/HOL/Tools/ATP/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/ATP/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
 ISABELLE_ATP="$COMPONENT"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -857,8 +857,9 @@
     val args' = map (rename_vars_term renaming) args
     val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     val _ = tracing ("Generated prolog program:\n" ^ prog)
-    val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
-      (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
+    val solution = TimeLimit.timeLimit timeout (fn prog =>
+      Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
+        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution
   in
--- a/src/HOL/Tools/Predicate_Compile/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,5 +1,8 @@
 # -*- shell-script -*- :mode=shellscript:
 
+# FIXME contrib_devel not official
+# FIXME $(type -p swipl) etc. does not allow spaces in file name
+
 EXEC_SWIPL="$(choosefrom \
   "$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
   "$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version	Mon Dec 20 17:31:58 2010 +0100
@@ -7,6 +7,9 @@
 if [ "$EXEC_SWIPL" = "" ]; then
   echo ""
 else
+  # FIXME does not allow spaces in $EXEC_SWIPL
+  # FIXME "expr match" not portable
+  # FIXME prefer $(...) in bash
   VERSION=`$EXEC_SWIPL --version`
   echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'`
 fi
--- a/src/HOL/Tools/SMT/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/SMT/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
 ISABELLE_SMT="$COMPONENT"
 
 REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
--- a/src/LCF/LCF.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/LCF/LCF.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -18,13 +18,13 @@
 
 typedecl tr
 typedecl void
-typedecl ('a,'b) "*"    (infixl "*" 6)
-typedecl ('a,'b) "+"    (infixl "+" 5)
+typedecl ('a,'b) prod  (infixl "*" 6)
+typedecl ('a,'b) sum  (infixl "+" 5)
 
 arities
   "fun" :: (cpo, cpo) cpo
-  "*" :: (cpo, cpo) cpo
-  "+" :: (cpo, cpo) cpo
+  prod :: (cpo, cpo) cpo
+  sum :: (cpo, cpo) cpo
   tr :: cpo
   void :: cpo
 
--- a/src/Pure/System/isabelle_system.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -7,10 +7,11 @@
 signature ISABELLE_SYSTEM =
 sig
   val isabelle_tool: string -> string -> int
-  val rm_tree: Path.T -> unit
   val mkdirs: Path.T -> unit
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
+  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -37,8 +38,6 @@
 
 (* directory operations *)
 
-fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
-
 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
 
 fun mkdir path =
@@ -48,5 +47,33 @@
   if File.eq (src, dst) then ()
   else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
+
+(* unique tmp files *)
+
+local
+
+fun fresh_path name =
+  let
+    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
+    val _ = File.exists path andalso
+      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
+  in path end;
+
+fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+
+in
+
+fun with_tmp_file name f =
+  let val path = fresh_path name
+  in Exn.release (Exn.capture f path before try File.rm path) end;
+
+fun with_tmp_dir name f =
+  let
+    val path = fresh_path name;
+    val _ = mkdirs path;
+  in Exn.release (Exn.capture f path before try rm_tree path) end;
+
 end;
 
+end;
+
--- a/src/Sequents/LK/Nat.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Sequents/LK/Nat.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -11,7 +11,7 @@
 
 typedecl nat
 arities nat :: "term"
-consts  "0" :: nat      ("0")
+consts  Zero :: nat      ("0")
         Suc :: "nat=>nat"
         rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
         add :: "[nat, nat] => nat"                (infixl "+" 60)
--- a/src/Tools/Code/code_target.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -397,7 +397,7 @@
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
-    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
+    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
 end; (* local *)
--- a/src/Tools/WWW_Find/etc/settings	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/WWW_Find/etc/settings	Mon Dec 20 17:31:58 2010 +0100
@@ -1,7 +1,8 @@
-# the path to lighttpd
+# -*- shell-script -*- :mode=shellscript:
+
 LIGHTTPD="/usr/sbin/lighttpd"
 
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-
 WWWFINDDIR="$COMPONENT"
 WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"
--- a/src/Tools/cache_io.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/cache_io.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -7,8 +7,6 @@
 signature CACHE_IO =
 sig
   (*IO wrapper*)
-  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
-  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   type result = {
     output: string list,
     redirected_output: string list,
@@ -34,21 +32,6 @@
 
 val cache_io_prefix = "cache-io-"
 
-fun with_tmp_file name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val x = Exn.capture f path
-    val _ = try File.rm path
-  in Exn.release x end
-
-fun with_tmp_dir name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val _ = Isabelle_System.mkdirs path
-    val x = Exn.capture f path
-    val _ = try Isabelle_System.rm_tree path
-  in Exn.release x end
-
 type result = {
   output: string list,
   redirected_output: string list,
@@ -62,8 +45,9 @@
   in {output=split_lines out2, redirected_output=out1, return_code=rc} end
 
 fun run make_cmd str =
-  with_tmp_file cache_io_prefix (fn in_path =>
-  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
+  Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
+    Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
+      raw_run make_cmd str in_path out_path))
 
 
 (* cache *)
--- a/src/ZF/Tools/datatype_package.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -91,7 +91,7 @@
   (** Define the constructors **)
 
   (*The empty tuple is 0*)
-  fun mk_tuple [] = @{const "0"}
+  fun mk_tuple [] = @{const zero}
     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
 
   fun mk_inject n k u = Balanced_Tree.access
--- a/src/ZF/Tools/induct_tacs.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -118,7 +118,7 @@
 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   let
     (*analyze the LHS of a case equation to get a constructor*)
-    fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
+    fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
       | const_of eqn = error ("Ill-formed case equation: " ^
                               Syntax.string_of_term_global thy eqn);
 
--- a/src/ZF/Tools/numeral_syntax.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -19,12 +19,12 @@
 
 (* bits *)
 
-fun mk_bit 0 = Syntax.const @{const_syntax "0"}
-  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
+fun mk_bit 0 = Syntax.const @{const_syntax zero}
+  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax zero}
   | mk_bit _ = raise Fail "mk_bit";
 
-fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
-  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
   | dest_bit _ = raise Match;
 
 
--- a/src/ZF/Tools/primrec_package.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -115,8 +115,8 @@
             case AList.lookup (op =) eqns cname of
                 NONE => (warning ("no equation for constructor " ^ cname ^
                                   "\nin definition of function " ^ fname);
-                         (Const (@{const_name 0}, Ind_Syntax.iT),
-                          #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
+                         (Const (@{const_name zero}, Ind_Syntax.iT),
+                          #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
               | SOME (rhs, cargs', eq) =>
                     (rhs, inst_recursor (recursor_pair, cargs'), eq)
           val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/ZF.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -17,7 +17,7 @@
 
 consts
 
-  "0"         :: "i"                  ("0")   --{*the empty set*}
+  zero        :: "i"                  ("0")   --{*the empty set*}
   Pow         :: "i => i"                     --{*power sets*}
   Inf         :: "i"                          --{*infinite set*}
 
--- a/src/ZF/arith_data.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/arith_data.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -24,7 +24,7 @@
 
 val iT = Ind_Syntax.iT;
 
-val zero = Const(@{const_name 0}, iT);
+val zero = Const(@{const_name zero}, iT);
 val succ = Const(@{const_name succ}, iT --> iT);
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
@@ -44,7 +44,7 @@
 
 (* dest_sum *)
 
-fun dest_sum (Const(@{const_name 0},_)) = []
+fun dest_sum (Const(@{const_name zero},_)) = []
   | dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
   | dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
   | dest_sum tm = [tm];
--- a/src/ZF/ind_syntax.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -29,7 +29,7 @@
 fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
 
 (*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
         error"Premises may not be conjuctive"
   | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
@@ -96,7 +96,7 @@
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = iT)
   in  case filter is_ind (args @ cs) of
-         [] => @{const 0}
+         [] => @{const zero}
        | u_args => Balanced_Tree.make mk_Un u_args
   end;
 
--- a/src/ZF/simpdata.ML	Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/simpdata.ML	Mon Dec 20 17:31:58 2010 +0100
@@ -32,8 +32,8 @@
 val ZF_conn_pairs =
   [(@{const_name Ball}, [@{thm bspec}]),
    (@{const_name All}, [@{thm spec}]),
-   (@{const_name "op -->"}, [@{thm mp}]),
-   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
+   (@{const_name imp}, [@{thm mp}]),
+   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
 
 (*Analyse a:b, where b is rigid*)
 val ZF_mem_pairs =