# HG changeset patch
# User haftmann
# Date 1282226934 -7200
# Node ID 9926c47ad1a1c282db731f38b9a28bc286b9be2f
# Parent  dc92eee56ed7ef5f806d567c46c5e12edd6b17b2
more antiquotations

diff -r dc92eee56ed7 -r 9926c47ad1a1 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 19 16:08:54 2010 +0200
@@ -1006,7 +1006,7 @@
 local
     val th = thm "not_def"
     val thy = theory_of_thm th
-    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
+    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
 in
 val not_elim_thm = Thm.combination pp th
 end
@@ -1052,9 +1052,9 @@
         val c = prop_of th3
         val vname = fst(dest_Free v)
         val (cold,cnew) = case c of
-                              tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
+                              tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
                               (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
-                            | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
+                            | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
                             | _ => raise ERR "mk_GEN" "Unknown conclusion"
         val th4 = Thm.rename_boundvars cold cnew th3
         val res = implies_intr_hyps th4
@@ -1204,7 +1204,8 @@
 
 fun non_trivial_term_consts t = fold_aterms
   (fn Const (c, _) =>
-      if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
+      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 ="}
       then I else insert (op =) c
     | _ => I) t [];
 
@@ -1212,12 +1213,12 @@
     let
         fun add_consts (Const (c, _), cs) =
             (case c of
-                 "op =" => insert (op =) "==" cs
-               | "op -->" => insert (op =) "==>" cs
-               | "All" => cs
+                 @{const_name "op ="} => insert (op =) "==" cs
+               | @{const_name "op -->"} => insert (op =) "==>" cs
+               | @{const_name All} => cs
                | "all" => cs
-               | "op &" => cs
-               | "Trueprop" => cs
+               | @{const_name "op &"} => cs
+               | @{const_name Trueprop} => cs
                | _ => insert (op =) c cs)
           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
           | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
@@ -1653,7 +1654,7 @@
         val cwit = cterm_of thy wit'
         val cty = ctyp_of_term cwit
         val a = case ex' of
-                    (Const(@{const_name "Ex"},_) $ a) => a
+                    (Const(@{const_name Ex},_) $ a) => a
                   | _ => raise ERR "EXISTS" "Argument not existential"
         val ca = cterm_of thy a
         val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
@@ -1686,7 +1687,7 @@
         val c = HOLogic.dest_Trueprop (concl_of th2)
         val cc = cterm_of thy c
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "Ex"},_) $ a) => a
+                    _ $ (Const(@{const_name Ex},_) $ a) => a
                   | _ => raise ERR "CHOOSE" "Conclusion not existential"
         val ca = cterm_of (theory_of_thm th1) a
         val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
@@ -1772,7 +1773,7 @@
         val (info',tm') = disamb_term_from info tm
         val th = norm_hyps th
         val ct = cterm_of thy tm'
-        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
+        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
         val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
         val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
         val res = HOLThm(rens_of info',res1)
@@ -1859,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 "op -->"},_) $ 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
@@ -1876,7 +1877,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 "Not"},_) $ a) => a
+                    _ $ (Const(@{const_name Not},_) $ a) => a
                   | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
         val ca = cterm_of thy a
         val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
@@ -1995,7 +1996,7 @@
                                        ("x",dT,body $ Bound 0)
                                    end
                                    handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
-                               fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
+                               fun dest_exists (Const(@{const_name Ex},_) $ abody) =
                                    dest_eta_abs abody
                                  | dest_exists tm =
                                    raise ERR "new_specification" "Bad existential formula"
@@ -2081,7 +2082,7 @@
             val (HOLThm(rens,td_th)) = norm_hthm thy hth
             val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
             val c = case concl_of th2 of
-                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
@@ -2107,7 +2108,7 @@
             val rew = rewrite_hol4_term (concl_of td_th) thy4
             val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
             val c   = case HOLogic.dest_Trueprop (prop_of th) of
-                          Const(@{const_name "Ex"},exT) $ P =>
+                          Const(@{const_name Ex},exT) $ P =>
                           let
                               val PT = domain_type exT
                           in
@@ -2156,7 +2157,7 @@
                                     SOME (cterm_of thy t)] light_nonempty
             val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
             val c = case concl_of th2 of
-                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = sort_strings (map fst tfrees)
diff -r dc92eee56ed7 -r 9926c47ad1a1 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Aug 19 16:08:54 2010 +0200
@@ -10,17 +10,17 @@
 exception not_HOHH;
 
 fun isD t = case t of
-    Const(@{const_name "Trueprop"},_)$t     => isD t
+    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(   "==>",_)$l$r     => isG l andalso isD r
-  | Const(@{const_name "All"},_)$Abs(s,_,t) => isD t
+  | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   | Const("all",_)$Abs(s,_,t) => isD t
   | Const(@{const_name "op |"},_)$_$_       => false
-  | Const(@{const_name "Ex"} ,_)$_          => false
-  | Const("not",_)$_          => false
-  | Const(@{const_name "True"},_)           => false
-  | Const(@{const_name "False"},_)          => false
+  | Const(@{const_name Ex} ,_)$_          => false
+  | Const(@{const_name Not},_)$_          => false
+  | Const(@{const_name True},_)           => false
+  | Const(@{const_name False},_)          => false
   | l $ r                     => isD l
   | Const _ (* rigid atom *)  => true
   | Bound _ (* rigid atom *)  => true
@@ -29,17 +29,17 @@
             anything else *)  => false
 and
     isG t = case t of
-    Const(@{const_name "Trueprop"},_)$t     => isG t
+    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(   "==>",_)$l$r     => isD l andalso isG r
-  | Const(@{const_name "All"},_)$Abs(_,_,t) => isG t
+  | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   | Const("all",_)$Abs(_,_,t) => isG t
-  | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
-  | Const(@{const_name "True"},_)           => true
-  | Const("not",_)$_          => false
-  | Const(@{const_name "False"},_)          => false
+  | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
+  | Const(@{const_name True},_)           => true
+  | Const(@{const_name Not},_)$_          => false
+  | Const(@{const_name False},_)          => false
   | _ (* atom *)              => true;
 
 val check_HOHH_tac1 = PRIMITIVE (fn thm =>
@@ -51,7 +51,7 @@
 
 fun atomizeD ctxt thm = let
     fun at  thm = case concl_of thm of
-      _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS
+      _$(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)
@@ -71,7 +71,7 @@
                                   resolve_tac (maps atomizeD prems) 1);
   -- 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))
+        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 t                          =                         (0,false,t);
 (*
@@ -79,7 +79,7 @@
         |   rep_goal (Const ("==>",_)$s$t)         =
                         (case rep_goal t of (l,t) => (s::l,t))
         |   rep_goal t                             = ([]  ,t);
-        val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
+        val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
                                                 (#3(dest_state (st,i)));
 *)
         val subgoal = #3(Thm.dest_state (st,i));
diff -r dc92eee56ed7 -r 9926c47ad1a1 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Thu Aug 19 16:08:54 2010 +0200
@@ -149,7 +149,7 @@
     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)) $ _)
-          = Term.strip_qnt_body "Ex" c
+          = Term.strip_qnt_body @{const_name Ex} c
       in cons r o cons l end
   in
     mk_skel (fold collect_pats cs [])
@@ -182,11 +182,11 @@
 fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
     val (sk, _, _, _, _) = D
-    val vs = Term.strip_qnt_vars "Ex" c
+    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)
-      = Term.strip_qnt_body "Ex" c
+      = Term.strip_qnt_body @{const_name Ex} c
     val (p, l') = dest_inj sk l
     val (q, r') = dest_inj sk r
   in
diff -r dc92eee56ed7 -r 9926c47ad1a1 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Aug 19 16:08:54 2010 +0200
@@ -149,21 +149,21 @@
 (*Are any of the logical connectives in "bs" present in the term?*)
 fun has_conns bs =
   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 "op |" orelse has p orelse has q
-        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
-        | has (Const(@{const_name "All"},_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
-        | has (Const(@{const_name "Ex"},_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
+        | 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 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
   in  has  end;
 
 
 (**** Clause handling ****)
 
-fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals P
+fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
   | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
-  | literals (Const(@{const_name "Not"},_) $ P) = [(false,P)]
+  | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   | literals P = [(true,P)];
 
 (*number of literals in a term*)
@@ -174,14 +174,14 @@
 
 fun signed_lits_aux (Const (@{const_name "op |"}, _) $ 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 (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
 
 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
 
 (*Literals like X=X are tautologous*)
 fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
-  | taut_poslit (Const(@{const_name "True"},_)) = true
+  | taut_poslit (Const(@{const_name True},_)) = true
   | taut_poslit _ = false;
 
 fun is_taut th =
@@ -210,7 +210,7 @@
        case HOLogic.dest_Trueprop (concl_of th) of
           (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
             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 "op |"}, _) $ (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*)
@@ -219,7 +219,7 @@
 
 fun notequal_lits_count (Const (@{const_name "op |"}, _) $ 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 (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -266,8 +266,8 @@
   fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
   
   (*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
+  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) =
         if b then sum (signed_nclauses b t) (signed_nclauses b u)
              else prod (signed_nclauses b t) (signed_nclauses b u)
@@ -284,8 +284,8 @@
                  else sum (prod (signed_nclauses b t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
         else 1
-    | signed_nclauses b (Const(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
-    | signed_nclauses b (Const(@{const_name "All"},_) $ Abs (_,_,t)) = signed_nclauses b t
+    | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
+    | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
     | signed_nclauses _ _ = 1; (* literal *)
  in 
   signed_nclauses true t >= max_cl
@@ -296,7 +296,7 @@
 local  
   val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
   val spec_varT = #T (Thm.rep_cterm spec_var);
-  fun name_of (Const (@{const_name "All"}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
+  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
 in  
   fun freeze_spec th ctxt =
     let
@@ -314,8 +314,7 @@
 
 (*Any need to extend this list with
   "HOL.type_class","HOL.eq_class","Pure.term"?*)
-val has_meta_conn =
-    exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
+val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
 
 fun apply_skolem_theorem (th, rls) =
   let
@@ -331,15 +330,15 @@
   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 ["All","Ex","op &"] (prop_of th))
+        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (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*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
-          | Const (@{const_name "All"}, _) => (*universal quantifier*)
+          | Const (@{const_name All}, _) => (*universal quantifier*)
                 let val (th',ctxt') = freeze_spec th (!ctxtr)
                 in  ctxtr := ctxt'; cnf_aux (th', ths) end
-          | Const (@{const_name "Ex"}, _) =>
+          | Const (@{const_name Ex}, _) =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
           | Const (@{const_name "op |"}, _) =>
@@ -365,7 +364,7 @@
 
 (**** Generation of contrapositives ****)
 
-fun is_left (Const (@{const_name "Trueprop"}, _) $
+fun is_left (Const (@{const_name Trueprop}, _) $
                (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
   | is_left _ = false;
 
@@ -401,8 +400,9 @@
 (*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 =)
-    ["Trueprop", "op &", "op |", "op -->", "Not",
-     "All", "Ex", @{const_name Ball}, @{const_name Bex}];
+    [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
+     @{const_name "op -->"}, @{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
   of any argument contains bool.*)
@@ -420,7 +420,7 @@
 (*Returns false if any Vars in the theorem mention type bool.
   Also rejects functions whose arguments are Booleans or other functions.*)
 fun is_fol_term thy t =
-    Term.is_first_order ["all","All","Ex"] t andalso
+    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
     not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
                            | _ => false) t orelse
          has_bool_arg_const t orelse
@@ -429,8 +429,8 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
-  | ok4horn (Const (@{const_name "Trueprop"},_) $ t) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+  | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   | ok4horn _ = false;
 
 (*Create a meta-level Horn clause*)
@@ -464,7 +464,7 @@
 
 (***** MESON PROOF PROCEDURE *****)
 
-fun rhyps (Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ phi,
+fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
            As) = rhyps(phi, A::As)
   | rhyps (_, As) = As;
 
@@ -509,8 +509,8 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun ok4nnf (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
-  | ok4nnf (Const (@{const_name "Trueprop"},_) $ t) = rigid t
+fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
+  | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
   | ok4nnf _ = false;
 
 fun make_nnf1 ctxt th =
@@ -546,7 +546,7 @@
 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   clauses that arise from a subgoal.*)
 fun skolemize1 ctxt th =
-  if not (has_conns ["Ex"] (prop_of th)) then th
+  if not (has_conns [@{const_name Ex}] (prop_of th)) then th
   else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
                               disj_exD, disj_exD1, disj_exD2])))
     handle THM ("tryres", _, _) =>
diff -r dc92eee56ed7 -r 9926c47ad1a1 src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 16:08:54 2010 +0200
@@ -122,7 +122,7 @@
       fun at thm =
           case concl_of thm of
             _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
-          | _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
+          | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
           | _                             => [thm];
     in map zero_var_indexes (at thm) end;
 
@@ -185,7 +185,7 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
 end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)