more antiquotations
authorhaftmann
Thu Aug 19 16:08:54 2010 +0200 (2010-08-19)
changeset 385579926c47ad1a1
parent 38556 dc92eee56ed7
child 38558 32ad17fe2b9c
more antiquotations
src/HOL/Import/proof_kernel.ML
src/HOL/Prolog/prolog.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/meson.ML
src/HOLCF/Tools/Domain/domain_library.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Aug 19 16:08:53 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 19 16:08:54 2010 +0200
     1.3 @@ -1006,7 +1006,7 @@
     1.4  local
     1.5      val th = thm "not_def"
     1.6      val thy = theory_of_thm th
     1.7 -    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
     1.8 +    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
     1.9  in
    1.10  val not_elim_thm = Thm.combination pp th
    1.11  end
    1.12 @@ -1052,9 +1052,9 @@
    1.13          val c = prop_of th3
    1.14          val vname = fst(dest_Free v)
    1.15          val (cold,cnew) = case c of
    1.16 -                              tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
    1.17 +                              tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
    1.18                                (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
    1.19 -                            | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
    1.20 +                            | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
    1.21                              | _ => raise ERR "mk_GEN" "Unknown conclusion"
    1.22          val th4 = Thm.rename_boundvars cold cnew th3
    1.23          val res = implies_intr_hyps th4
    1.24 @@ -1204,7 +1204,8 @@
    1.25  
    1.26  fun non_trivial_term_consts t = fold_aterms
    1.27    (fn Const (c, _) =>
    1.28 -      if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
    1.29 +      if c = @{const_name Trueprop} orelse c = @{const_name All}
    1.30 +        orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
    1.31        then I else insert (op =) c
    1.32      | _ => I) t [];
    1.33  
    1.34 @@ -1212,12 +1213,12 @@
    1.35      let
    1.36          fun add_consts (Const (c, _), cs) =
    1.37              (case c of
    1.38 -                 "op =" => insert (op =) "==" cs
    1.39 -               | "op -->" => insert (op =) "==>" cs
    1.40 -               | "All" => cs
    1.41 +                 @{const_name "op ="} => insert (op =) "==" cs
    1.42 +               | @{const_name "op -->"} => insert (op =) "==>" cs
    1.43 +               | @{const_name All} => cs
    1.44                 | "all" => cs
    1.45 -               | "op &" => cs
    1.46 -               | "Trueprop" => cs
    1.47 +               | @{const_name "op &"} => cs
    1.48 +               | @{const_name Trueprop} => cs
    1.49                 | _ => insert (op =) c cs)
    1.50            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    1.51            | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
    1.52 @@ -1653,7 +1654,7 @@
    1.53          val cwit = cterm_of thy wit'
    1.54          val cty = ctyp_of_term cwit
    1.55          val a = case ex' of
    1.56 -                    (Const(@{const_name "Ex"},_) $ a) => a
    1.57 +                    (Const(@{const_name Ex},_) $ a) => a
    1.58                    | _ => raise ERR "EXISTS" "Argument not existential"
    1.59          val ca = cterm_of thy a
    1.60          val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
    1.61 @@ -1686,7 +1687,7 @@
    1.62          val c = HOLogic.dest_Trueprop (concl_of th2)
    1.63          val cc = cterm_of thy c
    1.64          val a = case concl_of th1 of
    1.65 -                    _ $ (Const(@{const_name "Ex"},_) $ a) => a
    1.66 +                    _ $ (Const(@{const_name Ex},_) $ a) => a
    1.67                    | _ => raise ERR "CHOOSE" "Conclusion not existential"
    1.68          val ca = cterm_of (theory_of_thm th1) a
    1.69          val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
    1.70 @@ -1772,7 +1773,7 @@
    1.71          val (info',tm') = disamb_term_from info tm
    1.72          val th = norm_hyps th
    1.73          val ct = cterm_of thy tm'
    1.74 -        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
    1.75 +        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
    1.76          val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
    1.77          val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
    1.78          val res = HOLThm(rens_of info',res1)
    1.79 @@ -1859,7 +1860,7 @@
    1.80          val _ = if_debug pth hth
    1.81          val th1 = implies_elim_all (beta_eta_thm th)
    1.82          val a = case concl_of th1 of
    1.83 -                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
    1.84 +                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
    1.85                    | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
    1.86          val ca = cterm_of thy a
    1.87          val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
    1.88 @@ -1876,7 +1877,7 @@
    1.89          val _ = if_debug pth hth
    1.90          val th1 = implies_elim_all (beta_eta_thm th)
    1.91          val a = case concl_of th1 of
    1.92 -                    _ $ (Const(@{const_name "Not"},_) $ a) => a
    1.93 +                    _ $ (Const(@{const_name Not},_) $ a) => a
    1.94                    | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
    1.95          val ca = cterm_of thy a
    1.96          val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
    1.97 @@ -1995,7 +1996,7 @@
    1.98                                         ("x",dT,body $ Bound 0)
    1.99                                     end
   1.100                                     handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
   1.101 -                               fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
   1.102 +                               fun dest_exists (Const(@{const_name Ex},_) $ abody) =
   1.103                                     dest_eta_abs abody
   1.104                                   | dest_exists tm =
   1.105                                     raise ERR "new_specification" "Bad existential formula"
   1.106 @@ -2081,7 +2082,7 @@
   1.107              val (HOLThm(rens,td_th)) = norm_hthm thy hth
   1.108              val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
   1.109              val c = case concl_of th2 of
   1.110 -                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   1.111 +                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   1.112                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
   1.113              val tfrees = OldTerm.term_tfrees c
   1.114              val tnames = map fst tfrees
   1.115 @@ -2107,7 +2108,7 @@
   1.116              val rew = rewrite_hol4_term (concl_of td_th) thy4
   1.117              val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
   1.118              val c   = case HOLogic.dest_Trueprop (prop_of th) of
   1.119 -                          Const(@{const_name "Ex"},exT) $ P =>
   1.120 +                          Const(@{const_name Ex},exT) $ P =>
   1.121                            let
   1.122                                val PT = domain_type exT
   1.123                            in
   1.124 @@ -2156,7 +2157,7 @@
   1.125                                      SOME (cterm_of thy t)] light_nonempty
   1.126              val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
   1.127              val c = case concl_of th2 of
   1.128 -                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   1.129 +                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   1.130                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
   1.131              val tfrees = OldTerm.term_tfrees c
   1.132              val tnames = sort_strings (map fst tfrees)
     2.1 --- a/src/HOL/Prolog/prolog.ML	Thu Aug 19 16:08:53 2010 +0200
     2.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Aug 19 16:08:54 2010 +0200
     2.3 @@ -10,17 +10,17 @@
     2.4  exception not_HOHH;
     2.5  
     2.6  fun isD t = case t of
     2.7 -    Const(@{const_name "Trueprop"},_)$t     => isD t
     2.8 +    Const(@{const_name Trueprop},_)$t     => isD t
     2.9    | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
    2.10    | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
    2.11    | Const(   "==>",_)$l$r     => isG l andalso isD r
    2.12 -  | Const(@{const_name "All"},_)$Abs(s,_,t) => isD t
    2.13 +  | Const(@{const_name All},_)$Abs(s,_,t) => isD t
    2.14    | Const("all",_)$Abs(s,_,t) => isD t
    2.15    | Const(@{const_name "op |"},_)$_$_       => false
    2.16 -  | Const(@{const_name "Ex"} ,_)$_          => false
    2.17 -  | Const("not",_)$_          => false
    2.18 -  | Const(@{const_name "True"},_)           => false
    2.19 -  | Const(@{const_name "False"},_)          => false
    2.20 +  | Const(@{const_name Ex} ,_)$_          => false
    2.21 +  | Const(@{const_name Not},_)$_          => false
    2.22 +  | Const(@{const_name True},_)           => false
    2.23 +  | Const(@{const_name False},_)          => false
    2.24    | l $ r                     => isD l
    2.25    | Const _ (* rigid atom *)  => true
    2.26    | Bound _ (* rigid atom *)  => true
    2.27 @@ -29,17 +29,17 @@
    2.28              anything else *)  => false
    2.29  and
    2.30      isG t = case t of
    2.31 -    Const(@{const_name "Trueprop"},_)$t     => isG t
    2.32 +    Const(@{const_name Trueprop},_)$t     => isG t
    2.33    | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
    2.34    | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
    2.35    | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
    2.36    | Const(   "==>",_)$l$r     => isD l andalso isG r
    2.37 -  | Const(@{const_name "All"},_)$Abs(_,_,t) => isG t
    2.38 +  | Const(@{const_name All},_)$Abs(_,_,t) => isG t
    2.39    | Const("all",_)$Abs(_,_,t) => isG t
    2.40 -  | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
    2.41 -  | Const(@{const_name "True"},_)           => true
    2.42 -  | Const("not",_)$_          => false
    2.43 -  | Const(@{const_name "False"},_)          => false
    2.44 +  | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
    2.45 +  | Const(@{const_name True},_)           => true
    2.46 +  | Const(@{const_name Not},_)$_          => false
    2.47 +  | Const(@{const_name False},_)          => false
    2.48    | _ (* atom *)              => true;
    2.49  
    2.50  val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    2.51 @@ -51,7 +51,7 @@
    2.52  
    2.53  fun atomizeD ctxt thm = let
    2.54      fun at  thm = case concl_of thm of
    2.55 -      _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS
    2.56 +      _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
    2.57          (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    2.58      | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    2.59      | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
    2.60 @@ -71,7 +71,7 @@
    2.61                                    resolve_tac (maps atomizeD prems) 1);
    2.62    -- is nice, but cannot instantiate unknowns in the assumptions *)
    2.63  fun hyp_resolve_tac i st = let
    2.64 -        fun ap (Const(@{const_name "All"},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    2.65 +        fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    2.66          |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    2.67          |   ap t                          =                         (0,false,t);
    2.68  (*
    2.69 @@ -79,7 +79,7 @@
    2.70          |   rep_goal (Const ("==>",_)$s$t)         =
    2.71                          (case rep_goal t of (l,t) => (s::l,t))
    2.72          |   rep_goal t                             = ([]  ,t);
    2.73 -        val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
    2.74 +        val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
    2.75                                                  (#3(dest_state (st,i)));
    2.76  *)
    2.77          val subgoal = #3(Thm.dest_state (st,i));
     3.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Aug 19 16:08:53 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Aug 19 16:08:54 2010 +0200
     3.3 @@ -149,7 +149,7 @@
     3.4      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
     3.5        let
     3.6          val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
     3.7 -          = Term.strip_qnt_body "Ex" c
     3.8 +          = Term.strip_qnt_body @{const_name Ex} c
     3.9        in cons r o cons l end
    3.10    in
    3.11      mk_skel (fold collect_pats cs [])
    3.12 @@ -182,11 +182,11 @@
    3.13  fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    3.14    let
    3.15      val (sk, _, _, _, _) = D
    3.16 -    val vs = Term.strip_qnt_vars "Ex" c
    3.17 +    val vs = Term.strip_qnt_vars @{const_name Ex} c
    3.18  
    3.19      (* FIXME: throw error "dest_call" for malformed terms *)
    3.20      val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
    3.21 -      = Term.strip_qnt_body "Ex" c
    3.22 +      = Term.strip_qnt_body @{const_name Ex} c
    3.23      val (p, l') = dest_inj sk l
    3.24      val (q, r') = dest_inj sk r
    3.25    in
     4.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 19 16:08:53 2010 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 19 16:08:54 2010 +0200
     4.3 @@ -149,21 +149,21 @@
     4.4  (*Are any of the logical connectives in "bs" present in the term?*)
     4.5  fun has_conns bs =
     4.6    let fun has (Const(a,_)) = false
     4.7 -        | has (Const(@{const_name "Trueprop"},_) $ p) = has p
     4.8 -        | has (Const(@{const_name "Not"},_) $ p) = has p
     4.9 -        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
    4.10 -        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
    4.11 -        | has (Const(@{const_name "All"},_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
    4.12 -        | has (Const(@{const_name "Ex"},_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
    4.13 +        | has (Const(@{const_name Trueprop},_) $ p) = has p
    4.14 +        | has (Const(@{const_name Not},_) $ p) = has p
    4.15 +        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
    4.16 +        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
    4.17 +        | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
    4.18 +        | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
    4.19          | has _ = false
    4.20    in  has  end;
    4.21  
    4.22  
    4.23  (**** Clause handling ****)
    4.24  
    4.25 -fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals P
    4.26 +fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
    4.27    | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
    4.28 -  | literals (Const(@{const_name "Not"},_) $ P) = [(false,P)]
    4.29 +  | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
    4.30    | literals P = [(true,P)];
    4.31  
    4.32  (*number of literals in a term*)
    4.33 @@ -174,14 +174,14 @@
    4.34  
    4.35  fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
    4.36        signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
    4.37 -  | signed_lits_aux (Const(@{const_name "Not"},_) $ P) (poslits, neglits) = (poslits, P::neglits)
    4.38 +  | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
    4.39    | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
    4.40  
    4.41  fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
    4.42  
    4.43  (*Literals like X=X are tautologous*)
    4.44  fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
    4.45 -  | taut_poslit (Const(@{const_name "True"},_)) = true
    4.46 +  | taut_poslit (Const(@{const_name True},_)) = true
    4.47    | taut_poslit _ = false;
    4.48  
    4.49  fun is_taut th =
    4.50 @@ -210,7 +210,7 @@
    4.51         case HOLogic.dest_Trueprop (concl_of th) of
    4.52            (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
    4.53              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
    4.54 -        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
    4.55 +        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
    4.56              if eliminable(t,u)
    4.57              then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
    4.58              else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
    4.59 @@ -219,7 +219,7 @@
    4.60  
    4.61  fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
    4.62        notequal_lits_count P + notequal_lits_count Q
    4.63 -  | notequal_lits_count (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
    4.64 +  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
    4.65    | notequal_lits_count _ = 0;
    4.66  
    4.67  (*Simplify a clause by applying reflexivity to its negated equality literals*)
    4.68 @@ -266,8 +266,8 @@
    4.69    fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
    4.70    
    4.71    (*Estimate the number of clauses in order to detect infeasible theorems*)
    4.72 -  fun signed_nclauses b (Const(@{const_name "Trueprop"},_) $ t) = signed_nclauses b t
    4.73 -    | signed_nclauses b (Const(@{const_name "Not"},_) $ t) = signed_nclauses (not b) t
    4.74 +  fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
    4.75 +    | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
    4.76      | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
    4.77          if b then sum (signed_nclauses b t) (signed_nclauses b u)
    4.78               else prod (signed_nclauses b t) (signed_nclauses b u)
    4.79 @@ -284,8 +284,8 @@
    4.80                   else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    4.81                            (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    4.82          else 1
    4.83 -    | signed_nclauses b (Const(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
    4.84 -    | signed_nclauses b (Const(@{const_name "All"},_) $ Abs (_,_,t)) = signed_nclauses b t
    4.85 +    | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
    4.86 +    | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
    4.87      | signed_nclauses _ _ = 1; (* literal *)
    4.88   in 
    4.89    signed_nclauses true t >= max_cl
    4.90 @@ -296,7 +296,7 @@
    4.91  local  
    4.92    val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
    4.93    val spec_varT = #T (Thm.rep_cterm spec_var);
    4.94 -  fun name_of (Const (@{const_name "All"}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
    4.95 +  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
    4.96  in  
    4.97    fun freeze_spec th ctxt =
    4.98      let
    4.99 @@ -314,8 +314,7 @@
   4.100  
   4.101  (*Any need to extend this list with
   4.102    "HOL.type_class","HOL.eq_class","Pure.term"?*)
   4.103 -val has_meta_conn =
   4.104 -    exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
   4.105 +val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
   4.106  
   4.107  fun apply_skolem_theorem (th, rls) =
   4.108    let
   4.109 @@ -331,15 +330,15 @@
   4.110    let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
   4.111        fun cnf_aux (th,ths) =
   4.112          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   4.113 -        else if not (has_conns ["All","Ex","op &"] (prop_of th))
   4.114 +        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
   4.115          then nodups ctxt th :: ths (*no work to do, terminate*)
   4.116          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   4.117              Const (@{const_name "op &"}, _) => (*conjunction*)
   4.118                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   4.119 -          | Const (@{const_name "All"}, _) => (*universal quantifier*)
   4.120 +          | Const (@{const_name All}, _) => (*universal quantifier*)
   4.121                  let val (th',ctxt') = freeze_spec th (!ctxtr)
   4.122                  in  ctxtr := ctxt'; cnf_aux (th', ths) end
   4.123 -          | Const (@{const_name "Ex"}, _) =>
   4.124 +          | Const (@{const_name Ex}, _) =>
   4.125                (*existential quantifier: Insert Skolem functions*)
   4.126                cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
   4.127            | Const (@{const_name "op |"}, _) =>
   4.128 @@ -365,7 +364,7 @@
   4.129  
   4.130  (**** Generation of contrapositives ****)
   4.131  
   4.132 -fun is_left (Const (@{const_name "Trueprop"}, _) $
   4.133 +fun is_left (Const (@{const_name Trueprop}, _) $
   4.134                 (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
   4.135    | is_left _ = false;
   4.136  
   4.137 @@ -401,8 +400,9 @@
   4.138  (*Is the string the name of a connective? Really only | and Not can remain,
   4.139    since this code expects to be called on a clause form.*)
   4.140  val is_conn = member (op =)
   4.141 -    ["Trueprop", "op &", "op |", "op -->", "Not",
   4.142 -     "All", "Ex", @{const_name Ball}, @{const_name Bex}];
   4.143 +    [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
   4.144 +     @{const_name "op -->"}, @{const_name Not},
   4.145 +     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
   4.146  
   4.147  (*True if the term contains a function--not a logical connective--where the type
   4.148    of any argument contains bool.*)
   4.149 @@ -420,7 +420,7 @@
   4.150  (*Returns false if any Vars in the theorem mention type bool.
   4.151    Also rejects functions whose arguments are Booleans or other functions.*)
   4.152  fun is_fol_term thy t =
   4.153 -    Term.is_first_order ["all","All","Ex"] t andalso
   4.154 +    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
   4.155      not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
   4.156                             | _ => false) t orelse
   4.157           has_bool_arg_const t orelse
   4.158 @@ -429,8 +429,8 @@
   4.159  
   4.160  fun rigid t = not (is_Var (head_of t));
   4.161  
   4.162 -fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
   4.163 -  | ok4horn (Const (@{const_name "Trueprop"},_) $ t) = rigid t
   4.164 +fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
   4.165 +  | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   4.166    | ok4horn _ = false;
   4.167  
   4.168  (*Create a meta-level Horn clause*)
   4.169 @@ -464,7 +464,7 @@
   4.170  
   4.171  (***** MESON PROOF PROCEDURE *****)
   4.172  
   4.173 -fun rhyps (Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ phi,
   4.174 +fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   4.175             As) = rhyps(phi, A::As)
   4.176    | rhyps (_, As) = As;
   4.177  
   4.178 @@ -509,8 +509,8 @@
   4.179  val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   4.180                 not_impD, not_iffD, not_allD, not_exD, not_notD];
   4.181  
   4.182 -fun ok4nnf (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
   4.183 -  | ok4nnf (Const (@{const_name "Trueprop"},_) $ t) = rigid t
   4.184 +fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
   4.185 +  | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
   4.186    | ok4nnf _ = false;
   4.187  
   4.188  fun make_nnf1 ctxt th =
   4.189 @@ -546,7 +546,7 @@
   4.190  (*Pull existential quantifiers to front. This accomplishes Skolemization for
   4.191    clauses that arise from a subgoal.*)
   4.192  fun skolemize1 ctxt th =
   4.193 -  if not (has_conns ["Ex"] (prop_of th)) then th
   4.194 +  if not (has_conns [@{const_name Ex}] (prop_of th)) then th
   4.195    else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
   4.196                                disj_exD, disj_exD1, disj_exD2])))
   4.197      handle THM ("tryres", _, _) =>
     5.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 16:08:53 2010 +0200
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 16:08:54 2010 +0200
     5.3 @@ -122,7 +122,7 @@
     5.4        fun at thm =
     5.5            case concl_of thm of
     5.6              _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
     5.7 -          | _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
     5.8 +          | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
     5.9            | _                             => [thm];
    5.10      in map zero_var_indexes (at thm) end;
    5.11  
    5.12 @@ -185,7 +185,7 @@
    5.13  fun mk_lam  (x,T) = Abs(x,dummyT,T);
    5.14  fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
    5.15  fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
    5.16 -fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
    5.17 +fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
    5.18  end
    5.19  
    5.20  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)