merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
authorwenzelm
Fri, 27 Aug 2010 12:57:55 +0200
changeset 38797 abe92b33ac9f
parent 38796 c421cfe2eada (diff)
parent 38767 d8da44a8dd25 (current diff)
child 38798 89f273ab1d42
child 38815 d0196406ee32
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
NEWS
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/lin_arith.ML
src/HOL/ex/Numeral.thy
src/Pure/Isar/locale.ML
--- a/NEWS	Fri Aug 27 12:40:20 2010 +0200
+++ b/NEWS	Fri Aug 27 12:57:55 2010 +0200
@@ -120,6 +120,9 @@
     Trueprop ~> HOL.Trueprop
     True ~> HOL.True
     False ~> HOL.False
+    op & ~> HOL.conj
+    op | ~> HOL.disj
+    op --> ~> HOL.implies
     Not ~> HOL.Not
     The ~> HOL.The
     All ~> HOL.All
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -197,6 +197,7 @@
 apply (erule yahalom.induct,
        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
 done
 
 lemma analz_insert_freshK:
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -504,7 +504,7 @@
         in
           Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
         end) ||
-      binexp "implies" (binop @{term "op -->"}) ||
+      binexp "implies" (binop @{term HOL.implies}) ||
       scan_line "distinct" num :|-- scan_count exp >>
         (fn [] => @{term True}
           | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -50,11 +50,11 @@
 
 
 local
-  fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
+  fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u
     | explode_conj t = [t] 
 
-  fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
-    | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
+  fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
+    | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u)
     | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
     | splt (_, @{term True}) = []
     | splt tp = [tp]
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -59,12 +59,12 @@
     fun vc_of @{term True} = NONE
       | vc_of (@{term assert_at} $ Free (n, _) $ t) =
           SOME (Assert ((n, t), True))
-      | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
-      | vc_of (@{term "op -->"} $ t $ u) =
+      | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
+      | vc_of (@{term HOL.implies} $ t $ u) =
           vc_of u |> Option.map (assume t)
-      | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
+      | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
           SOME (vc_of u |> the_default True |> assert (n, t))
-      | vc_of (@{term "op &"} $ t $ u) =
+      | vc_of (@{term HOL.conj} $ t $ u) =
           (case (vc_of t, vc_of u) of
             (NONE, r) => r
           | (l, NONE) => l
@@ -74,9 +74,9 @@
 
 val prop_of_vc =
   let
-    fun mk_conj t u = @{term "op &"} $ t $ u
+    fun mk_conj t u = @{term HOL.conj} $ t $ u
 
-    fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
+    fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
       | term_of (Assert ((n, t), v)) =
           mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
       | term_of (Ignore v) = term_of v
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -3422,7 +3422,7 @@
 
 ML {*
   fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
-    | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
+    | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
     | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
     | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
     | calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $ 
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -1952,11 +1952,11 @@
         | NONE => error "num_of_term: unsupported dvd")
   | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term ps vs t')
@@ -2016,7 +2016,7 @@
 
 fun term_bools acc t =
   let
-    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+    val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "op = :: int => _"}, @{term "op < :: int => _"},
       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -1996,9 +1996,9 @@
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
   | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
   | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       @{code E} (fm_of_term (("", dummyT) :: vs) p)
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -5837,11 +5837,11 @@
       @{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
       @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term vs t')
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -2954,9 +2954,9 @@
 fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
 val brT = [bT, bT] ---> bT;
 val nott = @{term "Not"};
-val conjt = @{term "op &"};
-val disjt = @{term "op |"};
-val impt = @{term "op -->"};
+val conjt = @{term HOL.conj};
+val disjt = @{term HOL.disj};
+val impt = @{term HOL.implies};
 val ifft = @{term "op = :: bool => _"}
 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
 fun lle rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3018,9 +3018,9 @@
     Const(@{const_name True},_) => @{code T}
   | Const(@{const_name False},_) => @{code F}
   | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
-  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
-  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
-  | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op ="},ty)$p$q => 
        if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
        else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -33,12 +33,12 @@
              {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
 let
  fun uset (vars as (x::vs)) p = case term_of p of
-   Const(@{const_name "op &"}, _)$ _ $ _ =>
+   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
      in (lS@rS, Drule.binop_cong_rule b lth rth) end
- |  Const(@{const_name "op |"}, _)$ _ $ _ =>
+ |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
@@ -122,12 +122,12 @@
 
    fun decomp_mpinf fm =
      case term_of fm of
-       Const(@{const_name "op &"},_)$_$_ =>
+       Const(@{const_name HOL.conj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
-     | Const(@{const_name "op |"},_)$_$_ =>
+     | Const(@{const_name HOL.disj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
                          (Thm.cabs x p) (Thm.cabs x q))
@@ -181,9 +181,9 @@
    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
--- a/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -69,28 +69,28 @@
 val all_conjuncts = 
  let fun h acc ct = 
   case term_of ct of
-   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+   @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   | _ => ct::acc
 in h [] end;
 
 fun conjuncts ct =
  case term_of ct of
-  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
 | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
 
 fun mk_conj_tab th = 
  let fun h acc th = 
    case prop_of th of
-   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
+   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
      h (h acc (th RS conjunct2)) (th RS conjunct1)
   | @{term "Trueprop"}$p => (p,th)::acc
 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs = 
@@ -183,9 +183,9 @@
    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/HOL.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -57,13 +57,13 @@
   False         :: bool
   Not           :: "bool => bool"                   ("~ _" [40] 40)
 
+  conj          :: "[bool, bool] => bool"           (infixr "&" 35)
+  disj          :: "[bool, bool] => bool"           (infixr "|" 30)
+  implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
+
 setup Sign.root_path
 
 consts
-  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
-  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
-  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
-
   "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
 setup Sign.local_path
@@ -89,15 +89,15 @@
 
 notation (xsymbols)
   Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
-  "op -->"  (infixr "\<longrightarrow>" 25) and
+  HOL.conj  (infixr "\<and>" 35) and
+  HOL.disj  (infixr "\<or>" 30) and
+  HOL.implies  (infixr "\<longrightarrow>" 25) and
   not_equal  (infix "\<noteq>" 50)
 
 notation (HTML output)
   Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
+  HOL.conj  (infixr "\<and>" 35) and
+  HOL.disj  (infixr "\<or>" 30) and
   not_equal  (infix "\<noteq>" 50)
 
 abbreviation (iff)
@@ -184,7 +184,7 @@
 
 finalconsts
   "op ="
-  "op -->"
+  HOL.implies
   The
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -1578,7 +1578,7 @@
   val atomize_conjL = @{thm atomize_conjL}
   val atomize_disjL = @{thm atomize_disjL}
   val operator_names =
-    [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
+    [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
 );
 *}
 
@@ -1737,8 +1737,8 @@
   "True"    ("true")
   "False"   ("false")
   "Not"     ("Bool.not")
-  "op |"    ("(_ orelse/ _)")
-  "op &"    ("(_ andalso/ _)")
+  HOL.disj    ("(_ orelse/ _)")
+  HOL.conj    ("(_ andalso/ _)")
   "If"      ("(if _/ then _/ else _)")
 
 setup {*
@@ -1914,7 +1914,7 @@
   (Haskell "Bool")
   (Scala "Boolean")
 
-code_const True and False and Not and "op &" and "op |" and If
+code_const True and False and Not and HOL.conj and HOL.disj and If
   (SML "true" and "false" and "not"
     and infixl 1 "andalso" and infixl 0 "orelse"
     and "!(if (_)/ then (_)/ else (_))")
@@ -1924,7 +1924,7 @@
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
     and "!(if (_)/ then (_)/ else (_))")
-  (Scala "true" and "false" and "'!/ _"
+  (Scala "true" and "false" and "'! _"
     and infixl 3 "&&" and infixl 1 "||"
     and "!(if ((_))/ (_)/ else (_))")
 
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -484,11 +484,11 @@
 
 code_type array (Scala "!collection.mutable.ArraySeq[_]")
 code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
 
 end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -478,7 +478,6 @@
 
 code_include Scala "Heap"
 {*import collection.mutable.ArraySeq
-import Natural._
 
 def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 
@@ -487,24 +486,33 @@
 }
 
 object Ref {
-  def apply[A](x: A): Ref[A] = new Ref[A](x)
-  def lookup[A](r: Ref[A]): A = r.value
-  def update[A](r: Ref[A], x: A): Unit = { r.value = x }
+  def apply[A](x: A): Ref[A] =
+    new Ref[A](x)
+  def lookup[A](r: Ref[A]): A =
+    r.value
+  def update[A](r: Ref[A], x: A): Unit =
+    { r.value = x }
 }
 
 object Array {
-  def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
-  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
-  def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
-  def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
-  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
-  def freeze[A](a: ArraySeq[A]): List[A] = a.toList
+  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+    ArraySeq.fill(n.as_Int)(x)
+  def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
+    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
+  def len[A](a: ArraySeq[A]): Natural.Nat =
+    Natural.Nat(a.length)
+  def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
+    a(n.as_Int)
+  def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
+    a.update(n.as_Int, x)
+  def freeze[A](a: ArraySeq[A]): List[A] =
+    a.toList
 }*}
 
 code_reserved Scala bind Ref Array
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "bind")
+code_const bind (Scala "Heap.bind")
 code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error((_))")
 
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -306,10 +306,10 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Ref[_]")
+code_type ref (Scala "!Heap.Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
 
 end
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -17,8 +17,8 @@
   T               > True
   F               > False
   "!"             > All
-  "/\\"           > "op &"
-  "\\/"           > "op |"
+  "/\\"           > HOL.conj
+  "\\/"           > HOL.disj
   "?"             > Ex
   "?!"            > Ex1
   "~"             > Not
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -54,9 +54,9 @@
   ONE_ONE > HOL4Setup.ONE_ONE
   ONTO    > Fun.surj
   "=" > "op ="
-  "==>" > "op -->"
-  "/\\" > "op &"
-  "\\/" > "op |"
+  "==>" > HOL.implies
+  "/\\" > HOL.conj
+  "\\/" > HOL.disj
   "!" > All
   "?" > Ex
   "?!" > Ex1
--- a/src/HOL/Import/HOL/bool.imp	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Fri Aug 27 12:57:55 2010 +0200
@@ -14,7 +14,7 @@
 const_maps
   "~" > "HOL.Not"
   "bool_case" > "Datatype.bool.bool_case"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   "T" > "HOL.True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
@@ -30,7 +30,7 @@
   "ARB" > "HOL4Base.bool.ARB"
   "?!" > "HOL.Ex1"
   "?" > "HOL.Ex"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "!" > "HOL.All"
 
 thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 12:57:55 2010 +0200
@@ -115,7 +115,7 @@
   "_10303" > "HOLLight.hollight._10303"
   "_10302" > "HOLLight.hollight._10302"
   "_0" > "0" :: "nat"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
   "ZIP" > "HOLLight.hollight.ZIP"
   "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
@@ -233,11 +233,11 @@
   "?" > "HOL.Ex"
   ">=" > "HOLLight.hollight.>="
   ">" > "HOLLight.hollight.>"
-  "==>" > "op -->"
+  "==>" > HOL.implies
   "=" > "op ="
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "-" > "Groups.minus" :: "nat => nat => nat"
   "," > "Product_Type.Pair"
   "+" > "Groups.plus" :: "nat => nat => nat"
--- a/src/HOL/Import/hol4rews.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -628,7 +628,7 @@
             |> add_hol4_type_mapping "min" "fun" false "fun"
             |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
             |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
-            |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+            |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
             |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
 in
 val hol4_setup =
--- a/src/HOL/Import/proof_kernel.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -1205,7 +1205,7 @@
 fun non_trivial_term_consts t = fold_aterms
   (fn Const (c, _) =>
       if c = @{const_name Trueprop} orelse c = @{const_name All}
-        orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
       then I else insert (op =) c
     | _ => I) t [];
 
@@ -1214,10 +1214,10 @@
         fun add_consts (Const (c, _), cs) =
             (case c of
                  @{const_name "op ="} => insert (op =) "==" cs
-               | @{const_name "op -->"} => insert (op =) "==>" cs
+               | @{const_name HOL.implies} => insert (op =) "==>" cs
                | @{const_name All} => cs
                | "all" => cs
-               | @{const_name "op &"} => cs
+               | @{const_name HOL.conj} => cs
                | @{const_name Trueprop} => cs
                | _ => insert (op =) c cs)
           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
@@ -1521,7 +1521,7 @@
         val th1 = norm_hyps th1
         val th2 = norm_hyps th2
         val (l,r) = case concl_of th of
-                        _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
+                        _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
                       | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
         val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
         val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
@@ -1860,7 +1860,7 @@
         val _ = if_debug pth hth
         val th1 = implies_elim_all (beta_eta_thm th)
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
+                    _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
                   | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
         val ca = cterm_of thy a
         val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
--- a/src/HOL/Library/Code_Integer.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -51,14 +51,14 @@
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
-  (Scala "!(_/ -/ 1)")
+  (Scala "!(_ -/ 1)")
   (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
-  (Scala "!(_/ +/ 1)")
+  (Scala "!(_ +/ 1)")
   (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/Library/Code_Natural.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -9,9 +9,7 @@
 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
 
 code_include Haskell "Natural"
-{*import Data.Array.ST;
-
-newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
 
 instance Num Natural where {
   fromInteger k = Natural (if k >= 0 then k else 0);
@@ -54,48 +52,48 @@
 
 code_reserved Haskell Natural
 
-code_include Scala "Natural" {*
-import scala.Math
+code_include Scala "Natural"
+{*import scala.Math
 
-object Natural {
+object Nat {
 
-  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
-  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
-  def apply(numeral: String): Natural = Natural(BigInt(numeral))
+  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
+  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
+  def apply(numeral: String): Nat = Nat(BigInt(numeral))
 
 }
 
-class Natural private(private val value: BigInt) {
+class Nat private(private val value: BigInt) {
 
   override def hashCode(): Int = this.value.hashCode()
 
   override def equals(that: Any): Boolean = that match {
-    case that: Natural => this equals that
+    case that: Nat => this equals that
     case _ => false
   }
 
   override def toString(): String = this.value.toString
 
-  def equals(that: Natural): Boolean = this.value == that.value
+  def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
   def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
       this.value.intValue
     else error("Int value out of range: " + this.value.toString)
 
-  def +(that: Natural): Natural = new Natural(this.value + that.value)
-  def -(that: Natural): Natural = Natural(this.value - that.value)
-  def *(that: Natural): Natural = new Natural(this.value * that.value)
+  def +(that: Nat): Nat = new Nat(this.value + that.value)
+  def -(that: Nat): Nat = Nat(this.value - that.value)
+  def *(that: Nat): Nat = new Nat(this.value * that.value)
 
-  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
     else {
       val (k, l) = this.value /% that.value
-      (new Natural(k), new Natural(l))
+      (new Nat(k), new Nat(l))
     }
 
-  def <=(that: Natural): Boolean = this.value <= that.value
+  def <=(that: Nat): Boolean = this.value <= that.value
 
-  def <(that: Natural): Boolean = this.value < that.value
+  def <(that: Nat): Boolean = this.value < that.value
 
 }
 *}
@@ -104,7 +102,7 @@
 
 code_type code_numeral
   (Haskell "Natural.Natural")
-  (Scala "Natural")
+  (Scala "Natural.Nat")
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -242,8 +242,8 @@
   and @{typ int}.
 *}
 
-code_include Haskell "Nat" {*
-newtype Nat = Nat Integer deriving (Eq, Show, Read);
+code_include Haskell "Nat"
+{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
 
 instance Num Nat where {
   fromInteger k = Nat (if k >= 0 then k else 0);
@@ -280,8 +280,8 @@
 
 code_reserved Haskell Nat
 
-code_include Scala "Nat" {*
-import scala.Math
+code_include Scala "Nat"
+{*import scala.Math
 
 object Nat {
 
@@ -330,7 +330,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat")
+  (Scala "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -397,7 +397,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "Nat")
+  (Scala "!_.as'_BigInt" and "Nat.Nat")
 
 text {* Conversion from and to code numerals. *}
 
@@ -405,14 +405,14 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Natural(_.as'_BigInt)")
+  (Scala "!Natural.Nat(_.as'_BigInt)")
   (Eval "_")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Nat(_.as'_BigInt)")
+  (Scala "!Nat.Nat(_.as'_BigInt)")
   (Eval "_")
 
 text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -1356,7 +1356,7 @@
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term "op -->"}, @{term "op &"}, @{term "op |"},
+   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},
--- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -439,8 +439,8 @@
   val is_req = is_binop @{cterm "op =:: real => _"}
   val is_ge = is_binop @{cterm "op <=:: real => _"}
   val is_gt = is_binop @{cterm "op <:: real => _"}
-  val is_conj = is_binop @{cterm "op &"}
-  val is_disj = is_binop @{cterm "op |"}
+  val is_conj = is_binop @{cterm HOL.conj}
+  val is_disj = is_binop @{cterm HOL.disj}
   fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   fun disj_cases th th1 th2 = 
    let val (p,q) = Thm.dest_binop (concl th)
@@ -484,7 +484,7 @@
     val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
     val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
     val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
-    val th' = Drule.binop_cong_rule @{cterm "op |"} 
+    val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
     in Thm.transitive th th' 
@@ -542,12 +542,12 @@
   let 
    val nnf_norm_conv' = 
      nnf_conv then_conv 
-     literals_conv [@{term "op &"}, @{term "op |"}] [] 
+     literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
      (Conv.cache_conv 
        (first_conv [real_lt_conv, real_le_conv, 
                     real_eq_conv, real_not_lt_conv, 
                     real_not_le_conv, real_not_eq_conv, all_conv]))
-  fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] [] 
+  fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
                   (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
         try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
--- a/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -311,7 +311,7 @@
   shows "(\<Union> f) has_gmeasure (setsum m f)" using assms
 proof induct case (insert x s)
   have *:"(x \<inter> \<Union>s) = \<Union>{x \<inter> y| y. y\<in>s}"by auto
-  show ?case unfolding Union_insert ring_class.setsum.insert[OF insert(1-2)] 
+  show ?case unfolding Union_insert setsum.insert [OF insert(1-2)] 
     apply(rule has_gmeasure_negligible_union) unfolding *
     apply(rule insert) defer apply(rule insert) apply(rule insert) defer
     apply(rule insert) prefer 4 apply(rule negligible_unions)
--- a/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -4,7 +4,7 @@
 begin
 
 ML {*
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
 
 val forbidden =
  [(@{const_name Power.power}, "'a"),
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -187,7 +187,7 @@
 val nitpick_mtd = ("nitpick", invoke_nitpick)
 *)
 
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -1200,7 +1200,7 @@
           (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
     val tnames = Datatype_Prop.make_tnames recTs;
     val zs = Name.variant_list tnames (replicate (length descr'') "z");
-    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), tname), z) =>
         make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
         (descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1215,7 +1215,7 @@
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
           HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
             (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
-    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), tname), z) =>
         make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
         (descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1225,7 +1225,7 @@
       (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
        map mk_permT dt_atomTs) @ [("z", fsT')];
     val aux_ind_Ts = rev (map snd aux_ind_vars);
-    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn (((i, _), T), tname) =>
         HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
           fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -71,7 +71,7 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if member (op =) names name then SOME (f p q) else NONE
     | _ => NONE)
@@ -89,7 +89,7 @@
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
 
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -76,7 +76,7 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if member (op =) names name then SOME (f p q) else NONE
     | _ => NONE)
@@ -94,7 +94,7 @@
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
 
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Orderings.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Orderings.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -640,8 +640,8 @@
 let
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
-  val impl = @{const_syntax "op -->"};
-  val conj = @{const_syntax "op &"};
+  val impl = @{const_syntax HOL.implies};
+  val conj = @{const_syntax HOL.conj};
   val less = @{const_syntax less};
   val less_eq = @{const_syntax less_eq};
 
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -4,13 +4,24 @@
 
 section {* Example append *}
 
+
 inductive append
 where
   "append [] ys ys"
 | "append xs ys zs ==> append (x # xs) ys (x # zs)"
 
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
+values "{(x, y, z). append x y z}"
+
 values 3 "{(x, y, z). append x y z}"
 
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+
+values "{(x, y, z). append x y z}"
+
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
 
 section {* Example queens *}
 
@@ -172,7 +183,7 @@
 where
   "y \<noteq> B \<Longrightarrow> notB y"
 
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
 
 values 2 "{y. notB y}"
 
@@ -187,7 +198,7 @@
 inductive equals :: "abc => abc => bool"
 where
   "equals y' y'"
-ML {* set Code_Prolog.trace *}
+
 values 1 "{(y, z). equals y z}"
 
 end
--- a/src/HOL/Prolog/prolog.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -11,12 +11,12 @@
 
 fun isD t = case t of
     Const(@{const_name Trueprop},_)$t     => isD t
-  | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
-  | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
+  | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
+  | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
   | Const(   "==>",_)$l$r     => isG l andalso isD r
   | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   | Const("all",_)$Abs(s,_,t) => isD t
-  | Const(@{const_name "op |"},_)$_$_       => false
+  | Const(@{const_name HOL.disj},_)$_$_       => false
   | Const(@{const_name Ex} ,_)$_          => false
   | Const(@{const_name Not},_)$_          => false
   | Const(@{const_name True},_)           => false
@@ -30,9 +30,9 @@
 and
     isG t = case t of
     Const(@{const_name Trueprop},_)$t     => isG t
-  | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
-  | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
-  | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
+  | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
+  | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
+  | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   | Const(   "==>",_)$l$r     => isD l andalso isG r
   | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   | Const("all",_)$Abs(_,_,t) => isG t
@@ -53,8 +53,8 @@
     fun at  thm = case concl_of thm of
       _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
         (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
-    | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
-    | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
+    | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+    | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
     | _                             => [thm]
 in map zero_var_indexes (at thm) end;
 
@@ -72,7 +72,7 @@
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
         fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
-        |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
+        |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
         |   ap t                          =                         (0,false,t);
 (*
         fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
--- a/src/HOL/Set.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Set.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -219,8 +219,8 @@
   val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
-  val impl = @{const_syntax "op -->"};
-  val conj = @{const_syntax "op &"};
+  val impl = @{const_syntax HOL.implies};
+  val conj = @{const_syntax HOL.conj};
   val sbset = @{const_syntax subset};
   val sbset_eq = @{const_syntax subset_eq};
 
@@ -269,7 +269,7 @@
     fun setcompr_tr [e, idts, b] =
       let
         val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
-        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
+        val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
         val exP = ex_tr [idts, P];
       in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
 
@@ -288,7 +288,7 @@
   fun setcompr_tr' [Abs (abs as (_, _, P))] =
     let
       fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
-        | check (Const (@{const_syntax "op &"}, _) $
+        | check (Const (@{const_syntax HOL.conj}, _) $
               (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
             subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
@@ -305,7 +305,7 @@
           val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
         in
           case t of
-            Const (@{const_syntax "op &"}, _) $
+            Const (@{const_syntax HOL.conj}, _) $
               (Const (@{const_syntax Set.member}, _) $
                 (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
             if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
--- a/src/HOL/Statespace/state_fun.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -53,7 +53,7 @@
 val lazy_conj_simproc =
   Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
-      (case t of (Const (@{const_name "op &"},_)$P$Q) => 
+      (case t of (Const (@{const_name HOL.conj},_)$P$Q) => 
          let
             val P_P' = Simplifier.rewrite ss (cterm_of thy P);
             val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
--- a/src/HOL/TLA/Intensional.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -279,7 +279,7 @@
 
     fun hflatten t =
         case (concl_of t) of
-          Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
+          Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
         | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   in
     hflatten t
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -120,8 +120,8 @@
 fun split_conj_thm th =
   ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
 
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
+val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
+val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
 
 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
 
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -70,7 +70,7 @@
           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
         in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
-           foldr1 (HOLogic.mk_binop @{const_name "op &"})
+           foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
              (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
   in
@@ -149,7 +149,7 @@
     val prems = maps (fn ((i, (_, _, constrs)), T) =>
       map (make_ind_prem i T) constrs) (descr' ~~ recTs);
     val tnames = make_tnames recTs;
-    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
         (descr' ~~ recTs ~~ tnames)))
 
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -99,7 +99,7 @@
         if member (op =) is i then SOME
           (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
         else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
-    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
       (map (fn ((((i, _), T), U), tname) =>
         make_pred i U T (mk_proj i is r) (Free (tname, T)))
           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
--- a/src/HOL/Tools/Function/termination.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -148,7 +148,7 @@
     val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
-        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
           = Term.strip_qnt_body @{const_name Ex} c
       in cons r o cons l end
   in
@@ -185,7 +185,7 @@
     val vs = Term.strip_qnt_vars @{const_name Ex} c
 
     (* FIXME: throw error "dest_call" for malformed terms *)
-    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
       = Term.strip_qnt_body @{const_name Ex} c
     val (p, l') = dest_inj sk l
     val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -130,9 +130,9 @@
                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
          $ t1 $ t2 =>
          Subset (to_R_rep Ts t1, to_R_rep Ts t2)
-       | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
-       | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
-       | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
        | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
        | Free _ => raise SAME ()
        | Term.Var _ => raise SAME ()
@@ -173,12 +173,12 @@
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name ord_class.less_eq}, _) =>
          to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name bot_class.bot},
                 T as Type (@{type_name fun}, [_, @{typ bool}])) =>
          empty_n_ary_rel (arity_of RRep card T)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -386,13 +386,13 @@
     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   | strip_connective _ t = [t]
 fun strip_any_connective (t as (t0 $ _ $ _)) =
-    if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
+    if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
       (strip_connective t0 t, t0)
     else
       ([t], @{const Not})
   | strip_any_connective t = ([t], @{const Not})
-val conjuncts_of = strip_connective @{const "op &"}
-val disjuncts_of = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const HOL.conj}
+val disjuncts_of = strip_connective @{const HOL.disj}
 
 (* When you add constants to these lists, make sure to handle them in
    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -409,9 +409,9 @@
    (@{const_name All}, 1),
    (@{const_name Ex}, 1),
    (@{const_name "op ="}, 1),
-   (@{const_name "op &"}, 2),
-   (@{const_name "op |"}, 2),
-   (@{const_name "op -->"}, 2),
+   (@{const_name HOL.conj}, 2),
+   (@{const_name HOL.disj}, 2),
+   (@{const_name HOL.implies}, 2),
    (@{const_name If}, 3),
    (@{const_name Let}, 2),
    (@{const_name Pair}, 2),
@@ -1454,7 +1454,7 @@
   | @{const Trueprop} $ t1 => lhs_of_equation t1
   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
-  | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
+  | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   | _ => NONE
 fun is_constr_pattern _ (Bound _) = true
   | is_constr_pattern _ (Var _) = true
@@ -2148,8 +2148,8 @@
           fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
               Const (@{const_name Ex}, T1)
               $ Abs (s2, T2, repair_rec (j + 1) t2')
-            | repair_rec j (@{const "op &"} $ t1 $ t2) =
-              @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
+            | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
+              @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
             | repair_rec j t =
               let val (head, args) = strip_comb t in
                 if head = Bound j then
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -774,10 +774,10 @@
                         (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
                       end))
          | (t0 as Const (@{const_name All}, _))
-           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
+           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
          | (t0 as Const (@{const_name Ex}, _))
-           $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+           $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
          | Const (@{const_name Let}, _) $ t1 $ t2 =>
            do_term (betapply (t2, t1)) accum
@@ -883,12 +883,12 @@
            | (t0 as Const (s0, _)) $ t1 $ t2 =>
              if s0 = @{const_name "==>"} orelse
                 s0 = @{const_name Pure.conjunction} orelse
-                s0 = @{const_name "op &"} orelse
-                s0 = @{const_name "op |"} orelse
-                s0 = @{const_name "op -->"} then
+                s0 = @{const_name HOL.conj} orelse
+                s0 = @{const_name HOL.disj} orelse
+                s0 = @{const_name HOL.implies} then
                let
                  val impl = (s0 = @{const_name "==>"} orelse
-                             s0 = @{const_name "op -->"})
+                             s0 = @{const_name HOL.implies})
                  val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
                  val (m2, accum) = do_formula sn t2 accum
                in
@@ -975,8 +975,8 @@
             do_all t0 s0 T1 t1 accum
           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
             consider_general_equals mdata true x t1 t2 accum
-          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
-          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                              \do_formula", [t])
     in do_formula t end
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -518,11 +518,11 @@
         | (Const (@{const_name "op ="}, T), [t1]) =>
           Op1 (SingletonSet, range_type T, Any, sub t1)
         | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
-        | (Const (@{const_name "op &"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
           Op2 (And, bool_T, Any, sub' t1, sub' t2)
-        | (Const (@{const_name "op |"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, sub t1, sub t2)
-        | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
         | (Const (@{const_name If}, T), [t1, t2, t3]) =>
           Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -43,7 +43,7 @@
       | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
-      | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
+      | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
       | aux def (t as Const (s, _)) =
         (not def orelse t <> @{const Suc}) andalso
@@ -211,14 +211,14 @@
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | @{const "op &"} $ t1 $ t2 =>
-        @{const "op &"} $ do_term new_Ts old_Ts polar t1
+      | @{const HOL.conj} $ t1 $ t2 =>
+        @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
-      | @{const "op |"} $ t1 $ t2 =>
-        @{const "op |"} $ do_term new_Ts old_Ts polar t1
+      | @{const HOL.disj} $ t1 $ t2 =>
+        @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
-      | @{const "op -->"} $ t1 $ t2 =>
-        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+      | @{const HOL.implies} $ t1 $ t2 =>
+        @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
         $ do_term new_Ts old_Ts polar t2
       | Const (x as (s, T)) =>
         if is_descr s then
@@ -334,7 +334,7 @@
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
       | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+      | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -401,7 +401,7 @@
         t0 $ aux false t1 $ aux careful t2
       | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
         aux_eq careful true t0 t1 t2
-      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+      | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
       | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
       | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
@@ -449,7 +449,7 @@
 (** Destruction of universal and existential equalities **)
 
 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
-                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+                                   $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   | curry_assms (@{const "==>"} $ t1 $ t2) =
     @{const "==>"} $ curry_assms t1 $ curry_assms t2
@@ -604,12 +604,12 @@
           do_quantifier s0 T0 s1 T1 t1
         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | @{const "op &"} $ t1 $ t2 =>
+        | @{const HOL.conj} $ t1 $ t2 =>
           s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
-        | @{const "op |"} $ t1 $ t2 =>
+        | @{const HOL.disj} $ t1 $ t2 =>
           s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
-        | @{const "op -->"} $ t1 $ t2 =>
-          @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+        | @{const HOL.implies} $ t1 $ t2 =>
+          @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
           $ aux ss Ts js skolemizable polar t2
         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js skolemizable polar t2
@@ -620,8 +620,8 @@
             let
               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
               val (pref, connective) =
-                if gfp then (lbfp_prefix, @{const "op |"})
-                else (ubfp_prefix, @{const "op &"})
+                if gfp then (lbfp_prefix, @{const HOL.disj})
+                else (ubfp_prefix, @{const HOL.conj})
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
                            |> aux ss Ts js skolemizable polar
               fun neg () = Const (pref ^ s, T)
@@ -1105,7 +1105,7 @@
   case t of
     (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
     (case t1 of
-       (t10 as @{const "op &"}) $ t11 $ t12 =>
+       (t10 as @{const HOL.conj}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
      | (t10 as @{const Not}) $ t11 =>
@@ -1118,10 +1118,10 @@
          t0 $ Abs (s, T1, distribute_quantifiers t1))
   | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
     (case distribute_quantifiers t1 of
-       (t10 as @{const "op |"}) $ t11 $ t12 =>
+       (t10 as @{const HOL.disj}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+     | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
                                      $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -6,7 +6,9 @@
 
 signature CODE_PROLOG =
 sig
-  type code_options = {ensure_groundness : bool}
+  datatype prolog_system = SWI_PROLOG | YAP
+  type code_options =
+    {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
   val options : code_options ref
 
   datatype arith_op = Plus | Minus
@@ -21,10 +23,10 @@
   type clause = ((string * prol_term list) * prem);
   type logic_program = clause list;
   type constant_table = (string * string) list
-    
-  val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
+
+  val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
   val write_program : logic_program -> string
-  val run : logic_program -> string -> string list -> int option -> prol_term list list
+  val run : prolog_system -> logic_program -> string -> string list -> int option -> prol_term list list
 
   val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
 
@@ -42,9 +44,13 @@
 
 (* code generation options *)
 
-type code_options = {ensure_groundness : bool}
+datatype prolog_system = SWI_PROLOG | YAP
 
-val options = Unsynchronized.ref {ensure_groundness = false};
+type code_options =
+  {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+
+val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
+  prolog_system = SWI_PROLOG};
 
 (* general string functions *)
 
@@ -190,10 +196,10 @@
 
 fun mk_groundness_prems t = map Ground (Term.add_frees t [])
   
-fun translate_prem options ctxt constant_table t =  
+fun translate_prem ensure_groundness ctxt constant_table t =  
     case try HOLogic.dest_not t of
       SOME t =>
-        if #ensure_groundness options then
+        if ensure_groundness then
           Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
         else
           NegRel_of (translate_literal ctxt constant_table t)
@@ -215,7 +221,7 @@
       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
     (Thm.transfer thy rule)
 
-fun translate_intros options ctxt gr const constant_table =
+fun translate_intros ensure_groundness ctxt gr const constant_table =
   let
     val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
     val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
@@ -225,33 +231,11 @@
       let
         val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
         val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
-        val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
+        val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
         val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
       in clause end
   in (map translate_intro intros', constant_table') end
 
-val preprocess_options = Predicate_Compile_Aux.Options {
-  expected_modes = NONE,
-  proposed_modes = NONE,
-  proposed_names = [],
-  show_steps = false,
-  show_intermediate_results = false,
-  show_proof_trace = false,
-  show_modes = false,
-  show_mode_inference = false,
-  show_compilation = false,
-  show_caught_failures = false,
-  skip_proof = true,
-  no_topmost_reordering = false,
-  function_flattening = true,
-  specialise = false,
-  fail_safe_function_flattening = false,
-  no_higher_order_predicate = [],
-  inductify = false,
-  detect_switches = true,
-  compilation = Predicate_Compile_Aux.Pred
-}
-
 fun depending_preds_of (key, intros) =
   fold Term.add_const_names (map Thm.prop_of intros) []
 
@@ -272,7 +256,7 @@
     fst (extend' key (G, []))
   end
 
-fun generate options ctxt const =
+fun generate ensure_groundness ctxt const =
   let 
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -281,10 +265,11 @@
     val scc = strong_conn_of gr' [const]
     val constant_table = mk_constant_table (flat scc)
   in
-    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
+    apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
   end
   
-(* add implementation for ground predicates *)
+(* implementation for fully enumerating predicates and
+  for size-limited predicates for enumerating the values of a datatype upto a specific size *)
 
 fun add_ground_typ (Conj prems) = fold add_ground_typ prems
   | add_ground_typ (Ground (_, T)) = insert (op =) T
@@ -294,34 +279,58 @@
   first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
   | mk_relname _ = raise Fail "unexpected type"
 
+fun mk_lim_relname T = "lim_" ^  mk_relname T
+
 (* This is copied from "pat_completeness.ML" *)
 fun inst_constrs_of thy (T as Type (name, _)) =
   map (fn (Cn,CT) =>
     Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
     (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
+
+fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
   
-fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
+fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
   if member (op =) seen T then ([], (seen, constant_table))
   else
     let
-      val rel_name = mk_relname T
-      fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
+      val (limited, size) = case AList.lookup (op =) limited_types T of
+        SOME s => (true, s)
+      | NONE => (false, 0)      
+      val rel_name = (if limited then mk_lim_relname else mk_relname) T
+      fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
         let
           val constant_table' = declare_consts [constr_name] constant_table
+          val Ts = binder_types cT
           val (rec_clauses, (seen', constant_table'')) =
-            fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
-          val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))    
-          fun mk_prem v T = Rel (mk_relname T, [v])
+            fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table')
+          val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
+          val lim_var =
+            if limited then
+              if recursive then [AppF ("suc", [Var "Lim"])]              
+              else [Var "Lim"]
+            else [] 
+          fun mk_prem v T' =
+            if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
+            else Rel (mk_relname T', [v])
           val clause =
-            ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
-             Conj (map2 mk_prem vars (binder_types T)))
+            ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
+             Conj (map2 mk_prem vars Ts))
         in
           (clause :: flat rec_clauses, (seen', constant_table''))
         end
       val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
-    in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
- | mk_ground_impl ctxt T (seen, constant_table) =
+      val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
+        |> (fn cs => filter_out snd cs @ filter snd cs)
+      val (clauses, constant_table') =
+        apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table))
+      val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero")
+    in
+      ((if limited then
+        cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"]))
+      else I) clauses, constant_table')
+    end
+ | mk_ground_impl ctxt _ T (seen, constant_table) =
    raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
 
 fun replace_ground (Conj prems) = Conj (map replace_ground prems)
@@ -329,15 +338,16 @@
     Rel (mk_relname T, [Var x])  
   | replace_ground p = p
   
-fun add_ground_predicates ctxt (p, constant_table) =
+fun add_ground_predicates ctxt limited_types (p, constant_table) =
   let
     val ground_typs = fold (add_ground_typ o snd) p []
-    val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
+    val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
     val p' = map (apsnd replace_ground) p
   in
     ((flat grs) @ p', constant_table')
   end
-    
+
+  
 (* rename variables to prolog-friendly names *)
 
 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -396,14 +406,16 @@
 fun write_program p =
   cat_lines (map write_clause p) 
 
-(** query templates **)
+(* query templates *)
 
-fun query_first rel vnames =
+(** query and prelude for swi-prolog **)
+
+fun swi_prolog_query_first rel vnames =
   "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
   "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
   
-fun query_firstn n rel vnames =
+fun swi_prolog_query_firstn n rel vnames =
   "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
     rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
     "writelist([]).\n" ^
@@ -411,7 +423,7 @@
     "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
     "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
   
-val prelude =
+val swi_prolog_prelude =
   "#!/usr/bin/swipl -q -t main -f\n\n" ^
   ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   ":- style_check(-singleton).\n" ^
@@ -420,7 +432,38 @@
   "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   "main :- halt(1).\n"
 
+(** query and prelude for yap **)
+
+fun yap_query_first rel vnames =
+  "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
+  "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^
+  "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
+
+val yap_prelude =
+  "#!/usr/bin/yap -L\n\n" ^
+  ":- initialization(eval).\n"
+
+(* system-dependent query, prelude and invocation *)
+
+fun query system nsols = 
+  case system of
+    SWI_PROLOG =>
+      (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
+  | YAP =>
+      case nsols of NONE => yap_query_first | SOME n =>
+        error "No support for querying multiple solutions in the prolog system yap"
+
+fun prelude system =
+  case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
+
+fun invoke system file_name =
+  let
+    val cmd =
+      case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
+  in bash_output (cmd ^ file_name) end
+
 (* parsing prolog solution *)
+
 val scan_number =
   Scan.many1 Symbol.is_ascii_digit
 
@@ -471,26 +514,25 @@
   
 (* calling external interpreter and getting results *)
 
-fun run p query_rel vnames nsols =
+fun run system p query_rel vnames nsols =
   let
     val cmd = Path.named_root
-    val query = case nsols of NONE => query_first | SOME n => query_firstn n
     val p' = rename_vars_program p
     val _ = tracing "Renaming variable names..."
     val renaming = fold mk_renaming vnames [] 
     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
-    val prog = prelude ^ query query_rel vnames' ^ write_program p'
+    val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
     val _ = tracing ("Generated prolog program:\n" ^ prog)
     val prolog_file = File.tmp_path (Path.basic "prolog_file")
     val _ = File.write prolog_file prog
-    val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
+    val (solution, _) = invoke system (File.shell_path prolog_file)
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution
   in
     tss
   end
 
-(* values command *)
+(* restoring types in terms *)
 
 fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
   | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
@@ -509,6 +551,30 @@
         map (restore_term ctxt constant_table) (args ~~ argsT'))
     end
 
+(* values command *)
+
+val preprocess_options = Predicate_Compile_Aux.Options {
+  expected_modes = NONE,
+  proposed_modes = NONE,
+  proposed_names = [],
+  show_steps = false,
+  show_intermediate_results = false,
+  show_proof_trace = false,
+  show_modes = false,
+  show_mode_inference = false,
+  show_compilation = false,
+  show_caught_failures = false,
+  skip_proof = true,
+  no_topmost_reordering = false,
+  function_flattening = true,
+  specialise = false,
+  fail_safe_function_flattening = false,
+  no_higher_order_predicate = [],
+  inductify = false,
+  detect_switches = true,
+  compilation = Predicate_Compile_Aux.Pred
+}
+
 fun values ctxt soln t_compr =
   let
     val options = !options
@@ -535,10 +601,13 @@
       |> Predicate_Compile.preprocess preprocess_options t
     val ctxt' = ProofContext.init_global thy'
     val _ = tracing "Generating prolog program..."
-    val (p, constant_table) = generate options ctxt' name
-      |> (if #ensure_groundness options then add_ground_predicates ctxt' else I)
+    val (p, constant_table) = generate (#ensure_groundness options) ctxt' name
+      |> (if #ensure_groundness options then
+          add_ground_predicates ctxt' (#limited_types options)
+        else I)
     val _ = tracing "Running prolog program..."
-    val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
+    val tss = run (#prolog_system options)
+      p (translate_const constant_table name) (map first_upper vnames) soln
     val _ = tracing "Restoring terms..."
     val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
     fun mk_insert x S =
@@ -596,10 +665,10 @@
 
 (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
 
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
@@ -626,11 +695,11 @@
     val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
     val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
-    val (p, constant_table) = generate {ensure_groundness = true} ctxt' full_constname
-      |> add_ground_predicates ctxt'
+    val (p, constant_table) = generate true ctxt' full_constname
+      |> add_ground_predicates ctxt' (#limited_types (!options))
     val _ = tracing "Running prolog program..."
-    val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
-      (SOME 1)
+    val [ts] = run (#prolog_system (!options))
+      p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."
     val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
     val empty_report = ([], false)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -405,7 +405,7 @@
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
   | conjuncts_aux t conjs = t::conjs;
 
 fun conjuncts t = conjuncts_aux t [];
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -524,7 +524,7 @@
 
 fun dest_conjunct_prem th =
   case HOLogic.dest_Trueprop (prop_of th) of
-    (Const (@{const_name "op &"}, _) $ t $ t') =>
+    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
     | _ => [th]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -218,11 +218,11 @@
    @{const_name Trueprop},
    @{const_name Not},
    @{const_name "op ="},
-   @{const_name "op -->"},
+   @{const_name HOL.implies},
    @{const_name All},
    @{const_name Ex}, 
-   @{const_name "op &"},
-   @{const_name "op |"}]
+   @{const_name HOL.conj},
+   @{const_name HOL.disj}]
 
 fun special_cases (c, T) = member (op =) [
   @{const_name Product_Type.Unity},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -89,8 +89,8 @@
 fun is_compound ((Const (@{const_name Not}, _)) $ t) =
     error "is_compound: Negation should not occur; preprocessing is defect"
   | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
-  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
-  | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
+  | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
+  | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
     error "is_compound: Conjunction should not occur; preprocessing is defect"
   | is_compound _ = false
 
@@ -250,7 +250,7 @@
 
 fun split_conjs thy t =
   let 
-    fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+    fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
     (split_conjunctions t1) @ (split_conjunctions t2)
     | split_conjunctions t = [t]
   in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -168,10 +168,10 @@
     mk_split_lambda' xs t
   end;
 
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -28,7 +28,7 @@
    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
-   @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
+   @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, 
    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -120,8 +120,8 @@
 
 fun whatis x ct =
 ( case (term_of ct) of
-  Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
-| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+  Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
 | Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
 | Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
@@ -353,8 +353,8 @@
     then (ins (dest_number c) acc, dacc) else (acc,dacc)
   | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
     if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
-  | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
-  | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+  | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+  | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   | _ => (acc, dacc)
   val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
     end
   fun unit_conv t =
    case (term_of t) of
-   Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
-  | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
+   Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
+  | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
   | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
     if x=y andalso member (op =)
@@ -569,7 +569,7 @@
 fun add_bools t =
   let
     val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
-      @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+      @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
     val is_op = member (op =) ops;
@@ -612,11 +612,11 @@
 
 fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
   | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
-  | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
       Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
       Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
       Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
       Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -687,7 +687,7 @@
 
 fun strip_objimp ct =
   (case Thm.term_of ct of
-    Const (@{const_name "op -->"}, _) $ _ $ _ =>
+    Const (@{const_name HOL.implies}, _) $ _ $ _ =>
       let val (A, B) = Thm.dest_binop ct
       in A :: strip_objimp B end
   | _ => [ct]);
@@ -712,7 +712,7 @@
      val qs = filter P ps
      val q = if P c then c else @{cterm "False"}
      val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
-         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
+         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
      val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
      val ntac = (case qs of [] => q aconvc @{cterm "False"}
                          | _ => false)
--- a/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -25,8 +25,8 @@
    case (term_of p) of
     Const(s,T)$_$_ => 
        if domain_type T = HOLogic.boolT
-          andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
-            @{const_name "op -->"}, @{const_name "op ="}] s
+          andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
+            @{const_name HOL.implies}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
   | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -485,7 +485,7 @@
        end
 
   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
-      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+      (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
      Const (@{const_name Ex1}, ty') $ t') =>
        let
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -159,9 +159,9 @@
 fun conn @{const_name True} = SOME "true"
   | conn @{const_name False} = SOME "false"
   | conn @{const_name Not} = SOME "not"
-  | conn @{const_name "op &"} = SOME "and"
-  | conn @{const_name "op |"} = SOME "or"
-  | conn @{const_name "op -->"} = SOME "implies"
+  | conn @{const_name HOL.conj} = SOME "and"
+  | conn @{const_name HOL.disj} = SOME "or"
+  | conn @{const_name HOL.implies} = SOME "implies"
   | conn @{const_name "op ="} = SOME "iff"
   | conn @{const_name If} = SOME "if_then_else"
   | conn _ = NONE
--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -170,7 +170,7 @@
 val mk_true = @{cterm "~False"}
 val mk_false = @{cterm False}
 val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm "op -->"}
+val mk_implies = Thm.mk_binop @{cterm HOL.implies}
 val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
 
 fun mk_nary _ cu [] = cu
@@ -216,8 +216,8 @@
     (Sym ("true", _), []) => SOME mk_true
   | (Sym ("false", _), []) => SOME mk_false
   | (Sym ("not", _), [ct]) => SOME (mk_not ct)
-  | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
-  | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
+  | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
+  | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
   | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
   | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -62,14 +62,14 @@
 val is_neg = (fn @{term Not} $ _ => true | _ => false)
 fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
 val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
 
 fun dest_disj_term' f = (fn
-    @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
+    @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
   | _ => NONE)
 
-val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
 val dest_disj_term =
   dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
 
@@ -202,11 +202,11 @@
     | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
     | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
 
-  fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
+  fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
     | dest_conj t = raise TERM ("dest_conj", [t])
 
   val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
-  fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
+  fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
     | dest_disj t = raise TERM ("dest_disj", [t])
 
   val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -298,13 +298,13 @@
     let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
     in
       (case Thm.term_of ct1 of
-        @{term Not} $ (@{term "op &"} $ _ $ _) =>
+        @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
           prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
-      | @{term "op &"} $ _ $ _ =>
+      | @{term HOL.conj} $ _ $ _ =>
           prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
-      | @{term Not} $ (@{term "op |"} $ _ $ _) =>
+      | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
           prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
-      | @{term "op |"} $ _ $ _ =>
+      | @{term HOL.disj} $ _ $ _ =>
           prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
       | Const (@{const_name distinct}, _) $ _ =>
           let
@@ -477,8 +477,8 @@
 
   fun mono f (cp as (cl, _)) =
     (case Term.head_of (Thm.term_of cl) of
-      @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
-    | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
+      @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+    | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
     | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
     | _ => prove (prove_eq_safe f)) cp
 in
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -196,9 +196,9 @@
       | @{term True} => pair ct
       | @{term False} => pair ct
       | @{term Not} $ _ => abstr1 cvs ct
-      | @{term "op &"} $ _ $ _ => abstr2 cvs ct
-      | @{term "op |"} $ _ $ _ => abstr2 cvs ct
-      | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -68,8 +68,8 @@
         (*Universal quant: insert a free variable into body and continue*)
         let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
-      | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (prop_of th) []  end;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -95,9 +95,9 @@
   Symtab.make [(@{type_name Product_Type.prod}, "prod"),
                (@{type_name Sum_Type.sum}, "sum"),
                (@{const_name "op ="}, "equal"),
-               (@{const_name "op &"}, "and"),
-               (@{const_name "op |"}, "or"),
-               (@{const_name "op -->"}, "implies"),
+               (@{const_name HOL.conj}, "and"),
+               (@{const_name HOL.disj}, "or"),
+               (@{const_name HOL.implies}, "implies"),
                (@{const_name Set.member}, "member"),
                (@{const_name fequal}, "fequal"),
                (@{const_name COMBI}, "COMBI"),
@@ -430,7 +430,7 @@
 
 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
     literals_of_term1 args thy P
-  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
     literals_of_term1 (literals_of_term1 args thy P) thy Q
   | literals_of_term1 (lits, ts) thy P =
     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -159,9 +159,9 @@
         do_quantifier (pos = SOME false) body_t
       | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
         do_quantifier (pos = SOME true) body_t
-      | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
-      | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
-      | @{const "op -->"} $ t1 $ t2 =>
+      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const HOL.implies} $ t1 $ t2 =>
         do_formula (flip pos) t1 #> do_formula pos t2
       | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
         fold (do_term_or_formula T) [t1, t2]
@@ -541,12 +541,12 @@
       | (_, @{const "==>"} $ t1 $ t2) =>
         do_formula (not pos) t1 andalso
         (t2 = @{prop False} orelse do_formula pos t2)
-      | (_, @{const "op -->"} $ t1 $ t2) =>
+      | (_, @{const HOL.implies} $ t1 $ t2) =>
         do_formula (not pos) t1 andalso
         (t2 = @{const False} orelse do_formula pos t2)
       | (_, @{const Not} $ t1) => do_formula (not pos) t1
-      | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
-      | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
       | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
       | _ => false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -69,12 +69,12 @@
     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
-  | negate_term (@{const "op -->"} $ t1 $ t2) =
-    @{const "op &"} $ t1 $ negate_term t2
-  | negate_term (@{const "op &"} $ t1 $ t2) =
-    @{const "op |"} $ negate_term t1 $ negate_term t2
-  | negate_term (@{const "op |"} $ t1 $ t2) =
-    @{const "op &"} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const HOL.implies} $ t1 $ t2) =
+    @{const HOL.conj} $ t1 $ negate_term t2
+  | negate_term (@{const HOL.conj} $ t1 $ t2) =
+    @{const HOL.disj} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const HOL.disj} $ t1 $ t2) =
+    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   | negate_term (@{const Not} $ t) = t
   | negate_term t = @{const Not} $ t
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -70,9 +70,9 @@
         do_quant bs AForall s T t'
       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
         do_quant bs AExists s T t'
-      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
-      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
-      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
+      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
         do_conn bs AIff t1 t2
       | _ => (fn ts => do_term bs (Envir.eta_contract t)
@@ -125,9 +125,9 @@
             t0 $ Abs (s, T, aux (T :: Ts) t')
           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
             aux Ts (t0 $ eta_expand Ts t1 1)
-          | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
             t0 $ aux Ts t1 $ aux Ts t2
--- a/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -79,11 +79,11 @@
   in capply c (uncurry cabs r) end;
 
 
-local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
 end;
 
-local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
 end;
 
@@ -128,9 +128,9 @@
 val dest_neg    = dest_monop @{const_name Not}
 val dest_pair   = dest_binop @{const_name Pair}
 val dest_eq     = dest_binop @{const_name "op ="}
-val dest_imp    = dest_binop @{const_name "op -->"}
-val dest_conj   = dest_binop @{const_name "op &"}
-val dest_disj   = dest_binop @{const_name "op |"}
+val dest_imp    = dest_binop @{const_name HOL.implies}
+val dest_conj   = dest_binop @{const_name HOL.conj}
+val dest_disj   = dest_binop @{const_name HOL.disj}
 val dest_select = dest_binder @{const_name Eps}
 val dest_exists = dest_binder @{const_name Ex}
 val dest_forall = dest_binder @{const_name All}
--- a/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -159,7 +159,7 @@
 
 
 fun mk_imp{ant,conseq} =
-   let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[ant,conseq])
    end;
 
@@ -183,12 +183,12 @@
 
 
 fun mk_conj{conj1,conj2} =
-   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[conj1,conj2])
    end;
 
 fun mk_disj{disj1,disj2} =
-   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[disj1,disj2])
    end;
 
@@ -247,7 +247,7 @@
 fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
   | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
 
-fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
   | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
 
 fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
@@ -259,10 +259,10 @@
 fun dest_neg(Const(@{const_name Not},_) $ M) = M
   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
 
-fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
   | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
 
-fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
   | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
 
 fun mk_pair{fst,snd} =
--- a/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -95,9 +95,9 @@
 
 fun is_atom (Const (@{const_name False}, _))                                           = false
   | is_atom (Const (@{const_name True}, _))                                            = false
-  | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
-  | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
-  | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
+  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
+  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
+  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
   | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   | is_atom _                                                              = true;
@@ -105,7 +105,7 @@
 fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   | is_literal x                      = is_atom x;
 
-fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   | is_clause x                           = is_literal x;
 
 (* ------------------------------------------------------------------------- *)
@@ -184,21 +184,21 @@
 
 (* Theory.theory -> Term.term -> Thm.thm *)
 
-fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy y
 	in
 		conj_cong OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy y
 	in
 		disj_cong OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy y
@@ -218,21 +218,21 @@
 	make_nnf_not_false
   | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
 	make_nnf_not_true
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_conj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_disj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
@@ -276,7 +276,7 @@
 
 (* Theory.theory -> Term.term -> Thm.thm *)
 
-fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
 	let
 		val thm1 = simp_True_False_thm thy x
 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
 					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
 			end
 	end
-  | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
 	let
 		val thm1 = simp_True_False_thm thy x
 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
 fun make_cnf_thm thy t =
 let
 	(* Term.term -> Thm.thm *)
-	fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
+	fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
 		let
 			val thm1 = make_cnf_thm_from_nnf x
 			val thm2 = make_cnf_thm_from_nnf y
 		in
 			conj_cong OF [thm1, thm2]
 		end
-	  | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+	  | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
 		let
 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
-			fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+			fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
 				let
 					val thm1 = make_cnf_disj_thm x1 y'
 					val thm2 = make_cnf_disj_thm x2 y'
 				in
 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
 				end
-			  | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+			  | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
 				let
 					val thm1 = make_cnf_disj_thm x' y1
 					val thm2 = make_cnf_disj_thm x' y2
@@ -403,27 +403,27 @@
 	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
 	fun new_free () =
 		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
-	fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
+	fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
 		let
 			val thm1 = make_cnfx_thm_from_nnf x
 			val thm2 = make_cnfx_thm_from_nnf y
 		in
 			conj_cong OF [thm1, thm2]
 		end
-	  | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+	  | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
 		if is_clause x andalso is_clause y then
 			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
 		else if is_literal y orelse is_literal x then let
 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
 			(* almost in CNF, and x' or y' is a literal                      *)
-			fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+			fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
 				let
 					val thm1 = make_cnfx_disj_thm x1 y'
 					val thm2 = make_cnfx_disj_thm x2 y'
 				in
 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
 				end
-			  | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+			  | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
 				let
 					val thm1 = make_cnfx_disj_thm x' y1
 					val thm2 = make_cnfx_disj_thm x' y2
--- a/src/HOL/Tools/groebner.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -395,7 +395,7 @@
 
 fun refute_disj rfn tm =
  case term_of tm of
-  Const(@{const_name "op |"},_)$l$r =>
+  Const(@{const_name HOL.disj},_)$l$r =>
    compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   | _ => rfn tm ;
 
@@ -454,7 +454,7 @@
 val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
 
 val cTrp = @{cterm "Trueprop"};
-val cConj = @{cterm "op &"};
+val cConj = @{cterm HOL.conj};
 val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
 val assume_Trueprop = mk_comb cTrp #> assume;
 val list_mk_conj = list_mk_binop cConj;
@@ -479,22 +479,22 @@
   (* FIXME : copied from cqe.ML -- complex QE*)
 fun conjuncts ct =
  case term_of ct of
-  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
 | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
 
 fun mk_conj_tab th = 
  let fun h acc th = 
    case prop_of th of
-   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
+   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
      h (h acc (th RS conjunct2)) (th RS conjunct1)
   | @{term "Trueprop"}$p => (p,th)::acc
 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs = 
@@ -852,14 +852,14 @@
  fun unwind_polys_conv tm =
  let 
   val (vars,bod) = strip_exists tm
-  val cjs = striplist (dest_binary @{cterm "op &"}) bod
+  val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
   val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
              handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   val eq = Thm.lhs_of th1
-  val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
+  val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
   val th2 = conj_ac_rule (mk_eq bod bod')
   val th3 = transitive th2 
-         (Drule.binop_cong_rule @{cterm "op &"} th1 
+         (Drule.binop_cong_rule @{cterm HOL.conj} th1 
                 (reflexive (Thm.dest_arg (Thm.rhs_of th2))))
   val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
   val vars' = (remove op aconvc v vars) @ [v]
@@ -929,9 +929,9 @@
   | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
   | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
   | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
-  | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-  | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   | @{term "op ==>"} $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm
   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
--- a/src/HOL/Tools/hologic.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -208,29 +208,29 @@
   let val (th1, th2) = conj_elim th
   in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
 
-val conj = @{term "op &"}
-and disj = @{term "op |"}
-and imp = @{term "op -->"}
-and Not = @{term "Not"};
+val conj = @{term HOL.conj}
+and disj = @{term HOL.disj}
+and imp = @{term implies}
+and Not = @{term Not};
 
 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_not t = Not $ t;
 
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
-fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
   | dest_disj t = [t];
 
 (*Like dest_disj, but flattens disjunctions however nested*)
-fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   | disjuncts_aux t disjs = t::disjs;
 
 fun disjuncts t = disjuncts_aux t [];
 
-fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
+fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
 fun dest_not (Const ("HOL.Not", _) $ t) = t
--- a/src/HOL/Tools/inductive_set.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -74,9 +74,9 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop @{const_name "op &"} T x =
+      fun mkop @{const_name HOL.conj} T x =
             SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
-        | mkop @{const_name "op |"} T x =
+        | mkop @{const_name HOL.disj} T x =
             SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
--- a/src/HOL/Tools/lin_arith.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -45,7 +45,7 @@
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
 fun atomize thm = case Thm.prop_of thm of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   | _ => [thm];
 
--- a/src/HOL/Tools/meson.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -151,8 +151,8 @@
   let fun has (Const(a,_)) = false
         | has (Const(@{const_name Trueprop},_) $ p) = has p
         | has (Const(@{const_name Not},_) $ p) = has p
-        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
-        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
+        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
         | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
         | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
         | has _ = false
@@ -162,7 +162,7 @@
 (**** Clause handling ****)
 
 fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
-  | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
   | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   | literals P = [(true,P)];
 
@@ -172,7 +172,7 @@
 
 (*** Tautology Checking ***)
 
-fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
@@ -208,16 +208,16 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (concl_of th) of
-          (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
+          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
-        | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
         | _ => (*not a disjunction*) th;
 
-fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
       notequal_lits_count P + notequal_lits_count Q
   | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   | notequal_lits_count _ = 0;
@@ -268,13 +268,13 @@
   (*Estimate the number of clauses in order to detect infeasible theorems*)
   fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
     | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
-    | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
         if b then sum (signed_nclauses b t) (signed_nclauses b u)
              else prod (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
         if b then prod (signed_nclauses b t) (signed_nclauses b u)
              else sum (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
         if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
              else sum (signed_nclauses (not b) t) (signed_nclauses b u)
     | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
@@ -330,10 +330,10 @@
   let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
       fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
-        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
+        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
         then nodups ctxt th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
-            Const (@{const_name "op &"}, _) => (*conjunction*)
+            Const (@{const_name HOL.conj}, _) => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
           | Const (@{const_name All}, _) => (*universal quantifier*)
                 let val (th',ctxt') = freeze_spec th (!ctxtr)
@@ -341,7 +341,7 @@
           | Const (@{const_name Ex}, _) =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
-          | Const (@{const_name "op |"}, _) =>
+          | Const (@{const_name HOL.disj}, _) =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
               let val tac =
@@ -365,7 +365,7 @@
 (**** Generation of contrapositives ****)
 
 fun is_left (Const (@{const_name Trueprop}, _) $
-               (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
+               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -400,8 +400,8 @@
 (*Is the string the name of a connective? Really only | and Not can remain,
   since this code expects to be called on a clause form.*)
 val is_conn = member (op =)
-    [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
-     @{const_name "op -->"}, @{const_name Not},
+    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
+     @{const_name HOL.implies}, @{const_name Not},
      @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
 
 (*True if the term contains a function--not a logical connective--where the type
@@ -429,7 +429,7 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
   | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   | ok4horn _ = false;
 
--- a/src/HOL/Tools/prop_logic.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -397,14 +397,14 @@
 			(False, table)
 		  | aux (Const (@{const_name Not}, _) $ x)      table =
 			apfst Not (aux x table)
-		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1
 			in
 				(Or (fm1, fm2), table2)
 			end
-		  | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -342,7 +342,7 @@
     val bound_max = length Ts - 1;
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
-    fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
+    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
       | strip_imp A = ([], A)
     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
--- a/src/HOL/Tools/refute.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -648,9 +648,9 @@
       | Const (@{const_name All}, _) => t
       | Const (@{const_name Ex}, _) => t
       | Const (@{const_name "op ="}, _) => t
-      | Const (@{const_name "op &"}, _) => t
-      | Const (@{const_name "op |"}, _) => t
-      | Const (@{const_name "op -->"}, _) => t
+      | Const (@{const_name HOL.conj}, _) => t
+      | Const (@{const_name HOL.disj}, _) => t
+      | Const (@{const_name HOL.implies}, _) => t
       (* sets *)
       | Const (@{const_name Collect}, _) => t
       | Const (@{const_name Set.member}, _) => t
@@ -824,9 +824,9 @@
       | Const (@{const_name All}, T) => collect_type_axioms T axs
       | Const (@{const_name Ex}, T) => collect_type_axioms T axs
       | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
-      | Const (@{const_name "op &"}, _) => axs
-      | Const (@{const_name "op |"}, _) => axs
-      | Const (@{const_name "op -->"}, _) => axs
+      | Const (@{const_name HOL.conj}, _) => axs
+      | Const (@{const_name HOL.disj}, _) => axs
+      | Const (@{const_name HOL.implies}, _) => axs
       (* sets *)
       | Const (@{const_name Collect}, T) => collect_type_axioms T axs
       | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
@@ -1861,7 +1861,7 @@
       SOME (interpret thy model args (eta_expand t 1))
     | Const (@{const_name "op ="}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
-    | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
+    | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1871,14 +1871,14 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op &"}, _) $ t1 =>
+    | Const (@{const_name HOL.conj}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op &"}, _) =>
+    | Const (@{const_name HOL.conj}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False & undef":                                          *)
       (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
-    | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
+    | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1888,14 +1888,14 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op |"}, _) $ t1 =>
+    | Const (@{const_name HOL.disj}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op |"}, _) =>
+    | Const (@{const_name HOL.disj}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "True | undef":                                           *)
       (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
-    | Const (@{const_name "op -->"}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
+    | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1905,9 +1905,9 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op -->"}, _) $ t1 =>
+    | Const (@{const_name HOL.implies}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op -->"}, _) =>
+    | Const (@{const_name HOL.implies}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False --> undef":                                        *)
--- a/src/HOL/Tools/simpdata.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -12,9 +12,9 @@
   (*abstract syntax*)
   fun dest_eq ((c as Const(@{const_name "op ="},_)) $ 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 HOL.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 HOL.implies},_)) $ s $ t) = SOME (c, s, t)
     | dest_imp _ = NONE;
   val conj = HOLogic.conj
   val imp  = HOLogic.imp
@@ -159,8 +159,8 @@
   (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
 
 val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
-  (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name HOL.implies}, [@{thm mp}]),
+  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
   (@{const_name All}, [@{thm spec}]),
   (@{const_name True}, []),
   (@{const_name False}, []),
--- a/src/HOL/ex/Meson_Test.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) subset quotient union inter sum
+hide_const (open) implies union inter subset sum quotient 
 
 text {*
   Test data for the MESON proof procedure
--- a/src/HOL/ex/Numeral.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -1033,14 +1033,14 @@
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
-  (Scala "!(_/ -/ 1)")
+  (Scala "!(_ -/ 1)")
   (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
-  (Scala "!(_/ +/ 1)")
+  (Scala "!(_ +/ 1)")
   (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 12:57:55 2010 +0200
@@ -88,9 +88,9 @@
             else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
             else replace (c $ x $ y)   (*non-numeric comparison*)
     (*abstraction of a formula*)
-    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
       | fm ((c as Const(@{const_name True}, _))) = c
       | fm ((c as Const(@{const_name False}, _))) = c
--- a/src/HOL/ex/svc_funcs.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -89,9 +89,9 @@
    let fun tag t =
          let val (c,ts) = strip_comb t
          in  case c of
-             Const(@{const_name "op &"}, _)   => apply c (map tag ts)
-           | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
-           | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+             Const(@{const_name HOL.conj}, _)   => apply c (map tag ts)
+           | Const(@{const_name HOL.disj}, _)   => apply c (map tag ts)
+           | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
            | Const(@{const_name Not}, _)    => apply c (map tag ts)
            | Const(@{const_name True}, _)   => (c, false)
            | Const(@{const_name False}, _)  => (c, false)
@@ -183,11 +183,11 @@
       | tm t = Int (lit t)
                handle Match => var (t,[])
     (*translation of a formula*)
-    and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
+    and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
             Buildin("AND", [fm pos p, fm pos q])
-      | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
+      | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
             Buildin("OR", [fm pos p, fm pos q])
-      | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
+      | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
             Buildin("=>", [fm (not pos) p, fm pos q])
       | fm pos (Const(@{const_name Not}, _) $ p) =
             Buildin("NOT", [fm (not pos) p])
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -121,7 +121,7 @@
       val r_inst = read_instantiate ctxt;
       fun at thm =
           case concl_of thm of
-            _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+            _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
           | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
           | _                             => [thm];
     in map zero_var_indexes (at thm) end;
--- a/src/Pure/Isar/locale.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -483,7 +483,7 @@
     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
     val context' = Context.Theory thy';
     val (_, regs) = fold_rev (roundup thy' cons export)
-      (all_registrations context') (get_idents (context'), []);
+      (registrations_of context' loc) (get_idents (context'), []);
   in
     thy'
     |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
--- a/src/Tools/Code/code_haskell.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -261,9 +261,8 @@
           end;
   in print_stmt end;
 
-fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
+fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
   let
-    val module_alias = if is_some module_name then K module_name else raw_module_alias;
     val reserved = Name.make_context reserved;
     val mk_name_module = mk_name_module reserved module_prefix module_alias program;
     fun add_stmt (name, (stmt, deps)) =
@@ -314,15 +313,14 @@
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
-fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
-    raw_reserved includes raw_module_alias
-    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_haskell module_prefix module_name string_classes labelled_name
+    raw_reserved includes module_alias
+    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+    (stmt_names, presentation_stmt_names) destination =
   let
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
-    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
-      module_name module_prefix reserved raw_module_alias program;
+      module_prefix reserved module_alias program;
     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
     fun deriving_show tyco =
       let
@@ -344,11 +342,9 @@
       contr_classparam_typs
       (if string_classes then deriving_show else K false);
     fun print_module name content =
-      (name, Pretty.chunks [
+      (name, Pretty.chunks2 [
         str ("module " ^ name ^ " where {"),
-        str "",
         content,
-        str "",
         str "}"
       ]);
     fun serialize_module1 (module_name', (deps, (stmts, _))) =
--- a/src/Tools/Code/code_ml.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -489,7 +489,7 @@
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
-                (Pretty.block o Pretty.commas)
+                (Pretty.block o commas)
                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
                 str "->",
                 print_term is_pseudo_fun some_thm vars NOBR t
@@ -535,7 +535,7 @@
                       :: Pretty.brk 1
                       :: str "match"
                       :: Pretty.brk 1
-                      :: (Pretty.block o Pretty.commas) dummy_parms
+                      :: (Pretty.block o commas) dummy_parms
                       :: Pretty.brk 1
                       :: str "with"
                       :: Pretty.brk 1
@@ -722,9 +722,8 @@
 
 in
 
-fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved module_alias program =
   let
-    val module_alias = if is_some module_name then K module_name else raw_module_alias;
     val reserved = Name.make_context reserved;
     val empty_module = ((reserved, reserved), Graph.empty);
     fun map_node [] f = f
@@ -813,7 +812,7 @@
         ) stmts
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Datatype block without data statement: "
-                  ^ (commas o map (labelled_name o fst)) stmts)
+                  ^ (Library.commas o map (labelled_name o fst)) stmts)
              | stmts => ML_Datas stmts)));
     fun add_class stmts =
       fold_map
@@ -828,7 +827,7 @@
         ) stmts
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Class block without class statement: "
-                  ^ (commas o map (labelled_name o fst)) stmts)
+                  ^ (Library.commas o map (labelled_name o fst)) stmts)
              | [stmt] => ML_Class stmt)));
     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
           add_fun stmt
@@ -849,7 +848,7 @@
       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
           add_funs stmts
       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
-          (commas o map (labelled_name o fst)) stmts);
+          (Library.commas o map (labelled_name o fst)) stmts);
     fun add_stmts' stmts nsp_nodes =
       let
         val names as (name :: names') = map fst stmts;
@@ -858,9 +857,9 @@
         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
           handle Empty =>
             error ("Different namespace prefixes for mutual dependencies:\n"
-              ^ commas (map labelled_name names)
+              ^ Library.commas (map labelled_name names)
               ^ "\n"
-              ^ commas module_names);
+              ^ Library.commas module_names);
         val module_name_path = Long_Name.explode module_name;
         fun add_dep name name' =
           let
@@ -907,15 +906,14 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
-  reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
+  reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+  (stmt_names, presentation_stmt_names) =
   let
     val is_cons = Code_Thingol.is_cons program;
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
     val is_presentation = not (null presentation_stmt_names);
-    val module_name = if is_presentation then SOME "Code" else raw_module_name;
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
-      reserved raw_module_alias program;
+      reserved module_alias program;
     val reserved = make_vars reserved;
     fun print_node prefix (Dummy _) =
           NONE
@@ -939,7 +937,7 @@
   in
     Code_Target.mk_serialization target
       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
-      (rpair stmt_names' o code_of_pretty) p destination
+      (rpair stmt_names' o code_of_pretty) p
   end;
 
 end; (*local*)
@@ -948,8 +946,8 @@
 (** for instrumentalization **)
 
 fun evaluation_code_of thy target struct_name =
-  Code_Target.serialize_custom thy (target, fn _ => fn [] =>
-    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
+  Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
+    serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
 
 
 (** Isar setup **)
--- a/src/Tools/Code/code_printer.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -19,6 +19,7 @@
   val concat: Pretty.T list -> Pretty.T
   val brackets: Pretty.T list -> Pretty.T
   val enclose: string -> string -> Pretty.T list -> Pretty.T
+  val commas: Pretty.T list -> Pretty.T list
   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
   val semicolon: Pretty.T list -> Pretty.T
@@ -112,6 +113,7 @@
 fun xs @| y = xs @ [y];
 val str = Print_Mode.setmp [] Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
+val commas = Print_Mode.setmp [] Pretty.commas;
 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
--- a/src/Tools/Code/code_scala.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -25,7 +25,7 @@
 (** Scala serializer **)
 
 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
-    args_num is_singleton_constr deresolve =
+    args_num is_singleton_constr (deresolve, deresolve_full) =
   let
     val deresolve_base = Long_Name.base_name o deresolve;
     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
@@ -135,7 +135,7 @@
     fun print_context tyvars vs name = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
-          NOBR ((str o deresolve) name) vs;
+          NOBR ((str o deresolve_base) name) vs;
     fun print_defhead tyvars vars name vs params tys ty =
       Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
@@ -194,7 +194,8 @@
                 str "match", str "{"], str "}")
               (map print_clause eqs)
           end;
-    val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
+    val print_method = str o Library.enclose "`" "`" o space_implode "+"
+      o Long_Name.explode o deresolve_full;
     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
           print_def name (vs, ty) (filter (snd o snd) raw_eqs)
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
@@ -240,7 +241,7 @@
               in
                 concat [str "def", constraint (Pretty.block [applify "(" ")"
                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
                   add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
                   applify "(" ")" (str o lookup_var vars) NOBR
@@ -281,67 +282,137 @@
           end;
   in print_stmt end;
 
-fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
+local
+
+(* hierarchical module name space *)
+
+datatype node =
+    Dummy
+  | Stmt of Code_Thingol.stmt
+  | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
+
+in
+
+fun scala_program_of_program labelled_name reserved module_alias program =
   let
-    val the_module_name = the_default "Program" module_name;
-    val module_alias = K (SOME the_module_name);
-    val reserved = Name.make_context reserved;
-    fun prepare_stmt (name, stmt) (nsps, stmts) =
+
+    (* building module name hierarchy *)
+    fun alias_fragments name = case module_alias name
+     of SOME name' => Long_Name.explode name'
+      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
+          (Long_Name.explode name);
+    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
+    val fragments_tab = fold (fn name => Symtab.update
+      (name, alias_fragments name)) module_names Symtab.empty;
+    val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
+
+    (* building empty module hierarchy *)
+    val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
+    fun map_module f (Module content) = Module (f content);
+    fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
       let
-        val (_, base) = Code_Printer.dest_name name;
-        val mk_name_stmt = yield_singleton Name.variants;
-        fun add_class ((nsp_class, nsp_object), nsp_common) =
-          let
-            val (base', nsp_class') = mk_name_stmt base nsp_class
-          in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
-        fun add_object ((nsp_class, nsp_object), nsp_common) =
-          let
-            val (base', nsp_object') = mk_name_stmt base nsp_object
-          in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
-        fun add_common upper ((nsp_class, nsp_object), nsp_common) =
+        val declare = Name.declare name_fragement;
+      in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
+    fun ensure_module name_fragement (nsps, (implicits, nodes)) =
+      if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
+      else
+        (nsps |> declare_module name_fragement, (implicits,
+          nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
+    fun allocate_module [] = I
+      | allocate_module (name_fragment :: name_fragments) =
+          ensure_module name_fragment
+          #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+    val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
+      fragments_tab empty_module;
+    fun change_module [] = I
+      | change_module (name_fragment :: name_fragments) =
+          apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
+            o change_module name_fragments;
+
+    (* statement declaration *)
+    fun namify_class base ((nsp_class, nsp_object), nsp_common) =
+      let
+        val (base', nsp_class') = yield_singleton Name.variants base nsp_class
+      in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
+    fun namify_object base ((nsp_class, nsp_object), nsp_common) =
+      let
+        val (base', nsp_object') = yield_singleton Name.variants base nsp_object
+      in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
+    fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
+      let
+        val (base', nsp_common') =
+          yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
+      in
+        (base',
+          ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
+      end;
+    fun declare_stmt name stmt =
+      let
+        val (name_fragments, base) = dest_name name;
+        val namify = case stmt
+         of Code_Thingol.Fun _ => namify_object
+          | Code_Thingol.Datatype _ => namify_class
+          | Code_Thingol.Datatypecons _ => namify_common true
+          | Code_Thingol.Class _ => namify_class
+          | Code_Thingol.Classrel _ => namify_object
+          | Code_Thingol.Classparam _ => namify_object
+          | Code_Thingol.Classinst _ => namify_common false;
+        val stmt' = case stmt
+         of Code_Thingol.Datatypecons _ => Dummy
+          | Code_Thingol.Classrel _ => Dummy
+          | Code_Thingol.Classparam _ => Dummy
+          | _ => Stmt stmt;
+        fun is_classinst stmt = case stmt
+         of Code_Thingol.Classinst _ => true
+          | _ => false;
+        val implicit_deps = filter (is_classinst o Graph.get_node program)
+          (Graph.imm_succs program name);
+        fun declaration (nsps, (implicits, nodes)) =
           let
-            val (base', nsp_common') =
-              mk_name_stmt (if upper then first_upper base else base) nsp_common
-          in
-            (base',
-              ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
-          end;
-        val add_name = case stmt
-         of Code_Thingol.Fun _ => add_object
-          | Code_Thingol.Datatype _ => add_class
-          | Code_Thingol.Datatypecons _ => add_common true
-          | Code_Thingol.Class _ => add_class
-          | Code_Thingol.Classrel _ => add_object
-          | Code_Thingol.Classparam _ => add_object
-          | Code_Thingol.Classinst _ => add_common false;
-        fun add_stmt base' = case stmt
-         of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
-          | Code_Thingol.Classrel _ => cons (name, (base', NONE))
-          | Code_Thingol.Classparam _ => cons (name, (base', NONE))
-          | _ => cons (name, (base', SOME stmt));
-      in
-        nsps
-        |> add_name
-        |-> (fn base' => rpair (add_stmt base' stmts))
-      end;
-    val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
-      |> filter_out (Code_Thingol.is_case o snd);
-    val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
-    fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
-      handle Option => error ("Unknown statement name: " ^ labelled_name name);
-  in (deresolver, (the_module_name, sca_program)) end;
+            val (base', nsps') = namify base nsps;
+            val implicits' = union (op =) implicit_deps implicits;
+            val nodes' = Graph.new_node (name, (base', stmt')) nodes;
+          in (nsps', (implicits', nodes')) end;
+      in change_module name_fragments declaration end;
+
+    (* dependencies *)
+    fun add_dependency name name' =
+      let
+        val (name_fragments, base) = dest_name name;
+        val (name_fragments', base') = dest_name name';
+        val (name_fragments_common, (diff, diff')) =
+          chop_prefix (op =) (name_fragments, name_fragments');
+        val dep = if null diff then (name, name') else (hd diff, hd diff')
+      in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
+
+    (* producing program *)
+    val (_, (_, sca_program)) = empty_program
+      |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
+      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
 
-fun serialize_scala raw_module_name labelled_name
-    raw_reserved includes raw_module_alias
+    (* deresolving *)
+    fun deresolve name =
+      let
+        val (name_fragments, _) = dest_name name;
+        val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
+         of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
+        val (base', _) = Graph.get_node nodes name;
+      in Long_Name.implode (name_fragments @ [base']) end
+        handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
+
+  in (deresolve, sca_program) end;
+
+fun serialize_scala labelled_name raw_reserved includes module_alias
     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
-    program stmt_names destination =
+    program (stmt_names, presentation_stmt_names) destination =
   let
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
-    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
+
+    (* preprocess program *)
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
-    val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
-      module_name reserved raw_module_alias program;
-    val reserved = make_vars reserved;
+    val (deresolve, sca_program) = scala_program_of_program labelled_name
+      (Name.make_context reserved) module_alias program;
+
+    (* print statements *)
     fun lookup_constr tyco constr = case Graph.get_node program tyco
      of Code_Thingol.Datatype (_, (_, constrs)) =>
           the (AList.lookup (op = o apsnd fst) constrs constr);
@@ -359,44 +430,49 @@
      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
-      reserved args_num is_singleton_constr deresolver;
-    fun print_module name imports content =
-      (name, Pretty.chunks (
-        str ("object " ^ name ^ " {")
-        :: (if null imports then []
-          else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
-        @ [str "",
-        content,
-        str "",
-        str "}"]
-      ));
-    fun serialize_module the_module_name sca_program =
+      (make_vars reserved) args_num is_singleton_constr
+      (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
+
+    (* print nodes *)
+    fun print_implicit implicit =
       let
-        val content = Pretty.chunks2 (map_filter
-          (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
-            | (_, (_, NONE)) => NONE) sca_program);
-      in print_module the_module_name (map fst includes) content end;
-    fun check_destination destination =
-      (File.check destination; destination);
-    fun write_module destination (modlname, content) =
-      let
-        val filename = case modlname
-         of "" => Path.explode "Main.scala"
-          | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
-                o Long_Name.explode) modlname;
-        val pathname = Path.append destination filename;
-        val _ = File.mkdir_leaf (Path.dir pathname);
-      in File.write pathname (code_of_pretty content) end
+        val s = deresolve implicit;
+      in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
+    fun print_implicits implicits = case map_filter print_implicit implicits
+     of [] => NONE
+      | ps => (SOME o Pretty.block)
+          (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
+    fun print_module base implicits p = Pretty.chunks2
+      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
+        @ [p, str ("} /* object " ^ base ^ " */")]);
+    fun print_node (_, Dummy) = NONE
+      | print_node (name, Stmt stmt) = if null presentation_stmt_names
+          orelse member (op =) presentation_stmt_names name
+          then SOME (print_stmt (name, stmt))
+          else NONE
+      | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
+          then case print_nodes nodes
+           of NONE => NONE
+            | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
+          else print_nodes nodes
+    and print_nodes nodes = let
+        val ps = map_filter (fn name => print_node (name,
+          snd (Graph.get_node nodes name)))
+            ((rev o flat o Graph.strong_conn) nodes);
+      in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
+
+    (* serialization *)
+    val p_includes = if null presentation_stmt_names
+      then map (fn (base, p) => print_module base [] p) includes else [];
+    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
   in
     Code_Target.mk_serialization target
-      (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
-        (write_module (check_destination file)))
-      (rpair [] o cat_lines o map (code_of_pretty o snd))
-      (map (fn (name, content) => print_module name [] content) includes
-        @| serialize_module the_module_name sca_program)
-      destination
+      (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
+      (rpair [] o code_of_pretty) p destination
   end;
 
+end; (*local*)
+
 val literals = let
   fun char_scala c = if c = "'" then "\\'"
     else if c = "\"" then "\\\""
@@ -412,8 +488,8 @@
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
-  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
@@ -422,17 +498,17 @@
 
 (** Isar setup **)
 
-fun isar_serializer module_name =
+fun isar_serializer _ =
   Code_Target.parse_args (Scan.succeed ())
-  #> (fn () => serialize_scala module_name);
+  #> (fn () => serialize_scala);
 
 val setup =
   Code_Target.add_target
     (target, { serializer = isar_serializer, literals = literals,
-      check = { env_var = "SCALA_HOME", make_destination = I,
+      check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
         make_command = fn scala_home => fn p => fn _ =>
           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
-            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
+            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
   #> Code_Target.add_syntax_tyco target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -28,7 +28,7 @@
     -> 'a -> serialization
   val serialize: theory -> string -> int option -> string option -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
-  val serialize_custom: theory -> string * serializer
+  val serialize_custom: theory -> string * serializer -> string option
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val the_literals: theory -> string -> literals
   val export: serialization -> unit
@@ -111,7 +111,7 @@
   -> (string -> Code_Printer.activated_const_syntax option)
   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
-  -> string list                        (*selected statements*)
+  -> (string list * string list)        (*selected statements*)
   -> serialization;
 
 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
@@ -254,7 +254,7 @@
   |>> map_filter I;
 
 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
-    module_alias class instance tyco const module width args naming program2 names1 =
+    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
   let
     val (names_class, class') =
       activate_syntax (Code_Thingol.lookup_class naming) class;
@@ -275,14 +275,14 @@
     val _ = if null empty_funs then () else error ("No code equations for "
       ^ commas (map (Sign.extern_const thy) empty_funs));
   in
-    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
-      (Symtab.lookup module_alias) (Symtab.lookup class')
-      (Symtab.lookup tyco') (Symtab.lookup const')
+    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
+      (if is_some module_name then K module_name else Symtab.lookup module_alias)
+      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
       (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
-      program4 names1
+      program4 (names1, presentation_names)
   end;
 
-fun mount_serializer thy alt_serializer target some_width module args naming program names =
+fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
   let
     val ((targets, abortable), default_width) = Targets.get thy;
     fun collapse_hierarchy target =
@@ -299,6 +299,9 @@
     val (modify, data) = collapse_hierarchy target;
     val serializer = the_default (case the_description data
      of Fundamental seri => #serializer seri) alt_serializer;
+    val presentation_names = stmt_names_of_destination destination;
+    val module_name = if null presentation_names
+      then raw_module_name else SOME "Code";
     val reserved = the_reserved data;
     fun select_include names_all (name, (content, cs)) =
       if null cs then SOME (name, content)
@@ -308,13 +311,14 @@
       then SOME (name, content) else NONE;
     fun includes names_all = map_filter (select_include names_all)
       ((Symtab.dest o the_includes) data);
-    val module_alias = the_module_alias data;
+    val module_alias = the_module_alias data 
     val { class, instance, tyco, const } = the_name_syntax data;
     val literals = the_literals thy target;
     val width = the_default default_width some_width;
   in
     invoke_serializer thy abortable serializer literals reserved
-      includes module_alias class instance tyco const module width args naming (modify program) names
+      includes module_alias class instance tyco const module_name width args
+        naming (modify program) (names, presentation_names) destination
   end;
 
 in
@@ -344,8 +348,8 @@
     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
-fun serialize_custom thy (target_name, seri) naming program names =
-  mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
+fun serialize_custom thy (target_name, seri) module_name naming program names =
+  mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
   |> the;
 
 end; (* local *)
--- a/src/Tools/Code/code_thingol.ML	Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Aug 27 12:57:55 2010 +0200
@@ -271,9 +271,6 @@
        of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
         | NONE => Codegen.thyname_of_const thy c);
   fun purify_base "==>" = "follows"
-    | purify_base "op &" = "and"
-    | purify_base "op |" = "or"
-    | purify_base "op -->" = "implies"
     | purify_base "op =" = "eq"
     | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =