# HG changeset patch
# User wenzelm
# Date 1292859873 -3600
# Node ID 65631ca437c9d1c96bd82781e516d510ee4f11b0
# Parent  2e9bf718a7a1dbb0f59f27621dfe9003c9970a87
proper identifiers for consts and types;

diff -r 2e9bf718a7a1 -r 65631ca437c9 NEWS
--- a/NEWS	Mon Dec 20 15:24:25 2010 +0100
+++ b/NEWS	Mon Dec 20 16:44:33 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 ***
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/CTT/CTT.thy	Mon Dec 20 16:44:33 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<_,/_>)")
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/FOL.thy	Mon Dec 20 16:44:33 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
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/IFOL.thy	Mon Dec 20 16:44:33 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
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/ex/Nat.thy	Mon Dec 20 16:44:33 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)
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/fologic.ML	Mon Dec 20 16:44:33 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);
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/simpdata.ML	Mon Dec 20 16:44:33 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
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Dec 20 16:44:33 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}
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/ex/Nat.thy	Mon Dec 20 16:44:33 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)
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/simpdata.ML	Mon Dec 20 16:44:33 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}, [])];
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/HOL/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Dec 20 16:44:33 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"
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/HOL/Prolog/Test.thy	Mon Dec 20 16:44:33 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"
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/LCF/LCF.thy	Mon Dec 20 16:44:33 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
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/Sequents/LK/Nat.thy	Mon Dec 20 16:44:33 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)
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Dec 20 16:44:33 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
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Dec 20 16:44:33 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);
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Mon Dec 20 16:44:33 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;
 
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Mon Dec 20 16:44:33 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))
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/ZF.thy	Mon Dec 20 16:44:33 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*}
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/arith_data.ML	Mon Dec 20 16:44:33 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];
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Dec 20 16:44:33 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;
 
diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/simpdata.ML	Mon Dec 20 16:44:33 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 =