more qualified names;
authorwenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 5624584fc7dfa3cd4
parent 56244 3298b7a2795a
child 56246 2b2bcf4ecb48
more qualified names;
NEWS
src/CCL/Wfd.thy
src/Doc/ProgProve/LaTeXsugar.thy
src/FOL/simpdata.ML
src/FOLP/hypsubst.ML
src/FOLP/simp.ML
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/refute.ML
src/HOL/Matrix_LP/Compute_Oracle/compute.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Product_Type.thy
src/HOL/Prolog/prolog.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
src/HOL/Tools/Datatype/primrec.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_util.ML
src/HOL/Tools/SMT2/z3_new_proof.ML
src/HOL/Tools/SMT2/z3_new_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/record.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/Refute_Examples.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/Provers/blast.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/simple_syntax.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/conv.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/logic.ML
src/Pure/more_thm.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/raw_simplifier.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Sequents/simpdata.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_symbol.ML
src/Tools/induct.ML
src/Tools/misc_legacy.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
     1.1 --- a/NEWS	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/NEWS	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -71,6 +71,34 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Basic constants of Pure use more conventional names and are always
     1.8 +qualified.  Rare INCOMPATIBILITY, but with potentially serious
     1.9 +consequences, notably for tools in Isabelle/ML.  The following
    1.10 +renaming needs to be applied:
    1.11 +
    1.12 +  ==             ~>  Pure.eq
    1.13 +  ==>            ~>  Pure.imp
    1.14 +  all            ~>  Pure.all
    1.15 +  TYPE           ~>  Pure.type
    1.16 +  dummy_pattern  ~>  Pure.dummy_pattern
    1.17 +
    1.18 +Systematic porting works by using the following theory setup on a
    1.19 +*previous* Isabelle version to introduce the new name accesses for the
    1.20 +old constants:
    1.21 +
    1.22 +setup {*
    1.23 +  fn thy => thy
    1.24 +    |> Sign.root_path
    1.25 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
    1.26 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
    1.27 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
    1.28 +    |> Sign.restore_naming thy
    1.29 +*}
    1.30 +
    1.31 +Thus ML antiquotations like @{const_name Pure.eq} may be used already.
    1.32 +Later the application is moved to the current Isabelle version, and
    1.33 +the auxiliary aliases are deleted.
    1.34 +
    1.35  * Low-level type-class commands 'classes', 'classrel', 'arities' have
    1.36  been discontinued to avoid the danger of non-trivial axiomatization
    1.37  that is not immediately visible.  INCOMPATIBILITY, use regular
     2.1 --- a/src/CCL/Wfd.thy	Fri Mar 21 15:12:03 2014 +0100
     2.2 +++ b/src/CCL/Wfd.thy	Fri Mar 21 20:33:56 2014 +0100
     2.3 @@ -423,10 +423,10 @@
     2.4    @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
     2.5    @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
     2.6  
     2.7 -fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
     2.8 +fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l)
     2.9    | bvars _ l = l
    2.10  
    2.11 -fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
    2.12 +fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
    2.13    | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
    2.14    | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
    2.15    | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t
     3.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Fri Mar 21 15:12:03 2014 +0100
     3.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Fri Mar 21 20:33:56 2014 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  (* THEOREMS *)
     3.6  notation (Rule output)
     3.7 -  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
     3.8 +  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
     3.9  
    3.10  syntax (Rule output)
    3.11    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    3.12 @@ -28,7 +28,7 @@
    3.13    "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    3.14  
    3.15  notation (IfThen output)
    3.16 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    3.17 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    3.18  syntax (IfThen output)
    3.19    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    3.20    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    3.21 @@ -36,7 +36,7 @@
    3.22    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    3.23  
    3.24  notation (IfThenNoBox output)
    3.25 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    3.26 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    3.27  syntax (IfThenNoBox output)
    3.28    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    3.29    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
     4.1 --- a/src/FOL/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
     4.2 +++ b/src/FOL/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4    error("conclusion must be a =-equality or <->");;
     4.5  
     4.6  fun mk_eq th = case concl_of th of
     4.7 -    Const("==",_)$_$_           => th
     4.8 +    Const(@{const_name Pure.eq},_)$_$_ => th
     4.9    | _ $ (Const(@{const_name eq},_)$_$_)   => mk_meta_eq th
    4.10    | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
    4.11    | _ $ (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
     5.1 --- a/src/FOLP/hypsubst.ML	Fri Mar 21 15:12:03 2014 +0100
     5.2 +++ b/src/FOLP/hypsubst.ML	Fri Mar 21 20:33:56 2014 +0100
     5.3 @@ -58,8 +58,8 @@
     5.4     assumption.  Returns the number of intervening assumptions, paried with
     5.5     the rule asm_rl (resp. sym). *)
     5.6  fun eq_var bnd =
     5.7 -  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
     5.8 -        | eq_var_aux k (Const("==>",_) $ A $ B) =
     5.9 +  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
    5.10 +        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
    5.11                ((k, inspect_pair bnd (dest_eq A))
    5.12                        (*Exception Match comes from inspect_pair or dest_eq*)
    5.13                 handle Match => eq_var_aux (k+1) B)
     6.1 --- a/src/FOLP/simp.ML	Fri Mar 21 15:12:03 2014 +0100
     6.2 +++ b/src/FOLP/simp.ML	Fri Mar 21 20:33:56 2014 +0100
     6.3 @@ -405,10 +405,10 @@
     6.4      else ();
     6.5  
     6.6  (* Skip the first n hyps of a goal, and return the rest in generalized form *)
     6.7 -fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
     6.8 +fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) =
     6.9          if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
    6.10          else strip_varify(B,n-1,vs)
    6.11 -  | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
    6.12 +  | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) =
    6.13          strip_varify(t,n,Var(("?",length vs),T)::vs)
    6.14    | strip_varify  _  = [];
    6.15  
     7.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 15:12:03 2014 +0100
     7.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 20:33:56 2014 +0100
     7.3 @@ -84,7 +84,7 @@
     7.4      (* The result of the quantifier elimination *)
     7.5      val (th, tac) =
     7.6        (case (prop_of pre_thm) of
     7.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     7.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     7.9            let
    7.10              val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
    7.11            in
     8.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 15:12:03 2014 +0100
     8.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 20:33:56 2014 +0100
     8.3 @@ -64,7 +64,7 @@
     8.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     8.5      (* The result of the quantifier elimination *)
     8.6      val (th, tac) = case prop_of pre_thm of
     8.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     8.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     8.9      let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
    8.10      in 
    8.11         ((pth RS iffD2) RS pre_thm,
     9.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Mar 21 15:12:03 2014 +0100
     9.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Mar 21 20:33:56 2014 +0100
     9.3 @@ -184,9 +184,9 @@
     9.4     | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
     9.5     | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
     9.6     | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
     9.7 -   | Const ("==>", _) $ _ $ _ => find_args bounds tm
     9.8 -   | Const ("==", _) $ _ $ _ => find_args bounds tm
     9.9 -   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.10 +   | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
    9.11 +   | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
    9.12 +   | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.13     | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.14     | _ => Thm.dest_fun2 tm)
    9.15    and find_args bounds tm =
    10.1 --- a/src/HOL/Decision_Procs/langford.ML	Fri Mar 21 15:12:03 2014 +0100
    10.2 +++ b/src/HOL/Decision_Procs/langford.ML	Fri Mar 21 20:33:56 2014 +0100
    10.3 @@ -204,13 +204,13 @@
    10.4            else Thm.dest_fun2 tm
    10.5        | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    10.6        | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    10.7 -      | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    10.8 +      | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    10.9        | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.10        | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
   10.11        | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   10.12        | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   10.13 -      | Const ("==>", _) $ _ $ _ => find_args bounds tm
   10.14 -      | Const ("==", _) $ _ $ _ => find_args bounds tm
   10.15 +      | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
   10.16 +      | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
   10.17        | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
   10.18        | _ => Thm.dest_fun2 tm)
   10.19      and find_args bounds tm =
   10.20 @@ -230,7 +230,7 @@
   10.21  
   10.22  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   10.23    let
   10.24 -    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   10.25 +    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
   10.26      fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
   10.27      val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   10.28      val p' = fold_rev gen ts p
    11.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 21 15:12:03 2014 +0100
    11.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 21 20:33:56 2014 +0100
    11.3 @@ -112,7 +112,7 @@
    11.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    11.5      (* The result of the quantifier elimination *)
    11.6      val (th, tac) = case (prop_of pre_thm) of
    11.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    11.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    11.9      let val pth =
   11.10            (* If quick_and_dirty then run without proof generation as oracle*)
   11.11               if Config.get ctxt quick_and_dirty
    12.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Mar 21 15:12:03 2014 +0100
    12.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Mar 21 20:33:56 2014 +0100
    12.3 @@ -67,7 +67,7 @@
    12.4  
    12.5  (* THEOREMS *)
    12.6  notation (Rule output)
    12.7 -  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    12.8 +  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    12.9  
   12.10  syntax (Rule output)
   12.11    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   12.12 @@ -82,7 +82,7 @@
   12.13    "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
   12.14  
   12.15  notation (IfThen output)
   12.16 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   12.17 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   12.18  syntax (IfThen output)
   12.19    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   12.20    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   12.21 @@ -90,7 +90,7 @@
   12.22    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
   12.23  
   12.24  notation (IfThenNoBox output)
   12.25 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   12.26 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   12.27  syntax (IfThenNoBox output)
   12.28    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   12.29    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    13.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 15:12:03 2014 +0100
    13.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 20:33:56 2014 +0100
    13.3 @@ -33,7 +33,7 @@
    13.4  (* aligning equations *)
    13.5  notation (tab output)
    13.6    "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    13.7 -  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    13.8 +  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    13.9  
   13.10  (* Let *)
   13.11  translations 
    14.1 --- a/src/HOL/Library/refute.ML	Fri Mar 21 15:12:03 2014 +0100
    14.2 +++ b/src/HOL/Library/refute.ML	Fri Mar 21 20:33:56 2014 +0100
    14.3 @@ -545,9 +545,9 @@
    14.4      fun unfold_loop t =
    14.5        case t of
    14.6        (* Pure *)
    14.7 -        Const (@{const_name all}, _) => t
    14.8 -      | Const (@{const_name "=="}, _) => t
    14.9 -      | Const (@{const_name "==>"}, _) => t
   14.10 +        Const (@{const_name Pure.all}, _) => t
   14.11 +      | Const (@{const_name Pure.eq}, _) => t
   14.12 +      | Const (@{const_name Pure.imp}, _) => t
   14.13        | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
   14.14        (* HOL *)
   14.15        | Const (@{const_name Trueprop}, _) => t
   14.16 @@ -709,9 +709,9 @@
   14.17      and collect_term_axioms t axs =
   14.18        case t of
   14.19        (* Pure *)
   14.20 -        Const (@{const_name all}, _) => axs
   14.21 -      | Const (@{const_name "=="}, _) => axs
   14.22 -      | Const (@{const_name "==>"}, _) => axs
   14.23 +        Const (@{const_name Pure.all}, _) => axs
   14.24 +      | Const (@{const_name Pure.eq}, _) => axs
   14.25 +      | Const (@{const_name Pure.imp}, _) => axs
   14.26        (* axiomatic type classes *)
   14.27        | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
   14.28        (* HOL *)
   14.29 @@ -1183,7 +1183,7 @@
   14.30      (* interpretation which includes values for the (formerly)           *)
   14.31      (* quantified variables.                                             *)
   14.32      (* maps  !!x1...xn. !xk...xm. t   to   t  *)
   14.33 -    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
   14.34 +    fun strip_all_body (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) =
   14.35            strip_all_body t
   14.36        | strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
   14.37            strip_all_body t
   14.38 @@ -1191,7 +1191,7 @@
   14.39            strip_all_body t
   14.40        | strip_all_body t = t
   14.41      (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)
   14.42 -    fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
   14.43 +    fun strip_all_vars (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) =
   14.44            (a, T) :: strip_all_vars t
   14.45        | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) =
   14.46            strip_all_vars t
   14.47 @@ -1569,7 +1569,7 @@
   14.48  
   14.49  fun Pure_interpreter ctxt model args t =
   14.50    case t of
   14.51 -    Const (@{const_name all}, _) $ t1 =>
   14.52 +    Const (@{const_name Pure.all}, _) $ t1 =>
   14.53        let
   14.54          val (i, m, a) = interpret ctxt model args t1
   14.55        in
   14.56 @@ -1584,11 +1584,11 @@
   14.57              end
   14.58          | _ =>
   14.59            raise REFUTE ("Pure_interpreter",
   14.60 -            "\"all\" is followed by a non-function")
   14.61 +            "\"Pure.all\" is followed by a non-function")
   14.62        end
   14.63 -  | Const (@{const_name all}, _) =>
   14.64 +  | Const (@{const_name Pure.all}, _) =>
   14.65        SOME (interpret ctxt model args (eta_expand t 1))
   14.66 -  | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   14.67 +  | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
   14.68        let
   14.69          val (i1, m1, a1) = interpret ctxt model args t1
   14.70          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   14.71 @@ -1597,11 +1597,11 @@
   14.72          SOME ((if #def_eq args then make_def_equality else make_equality)
   14.73            (i1, i2), m2, a2)
   14.74        end
   14.75 -  | Const (@{const_name "=="}, _) $ _ =>
   14.76 +  | Const (@{const_name Pure.eq}, _) $ _ =>
   14.77        SOME (interpret ctxt model args (eta_expand t 1))
   14.78 -  | Const (@{const_name "=="}, _) =>
   14.79 +  | Const (@{const_name Pure.eq}, _) =>
   14.80        SOME (interpret ctxt model args (eta_expand t 2))
   14.81 -  | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
   14.82 +  | Const (@{const_name Pure.imp}, _) $ t1 $ t2 =>
   14.83        (* 3-valued logic *)
   14.84        let
   14.85          val (i1, m1, a1) = interpret ctxt model args t1
   14.86 @@ -1611,9 +1611,9 @@
   14.87        in
   14.88          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   14.89        end
   14.90 -  | Const (@{const_name "==>"}, _) $ _ =>
   14.91 +  | Const (@{const_name Pure.imp}, _) $ _ =>
   14.92        SOME (interpret ctxt model args (eta_expand t 1))
   14.93 -  | Const (@{const_name "==>"}, _) =>
   14.94 +  | Const (@{const_name Pure.imp}, _) =>
   14.95        SOME (interpret ctxt model args (eta_expand t 2))
   14.96    | _ => NONE;
   14.97  
   14.98 @@ -1632,7 +1632,7 @@
   14.99    (* redundant, since 'False' is also an IDT constructor *)
  14.100    | Const (@{const_name False}, _) =>
  14.101        SOME (FF, model, args)
  14.102 -  | Const (@{const_name All}, _) $ t1 =>  (* similar to "all" (Pure) *)
  14.103 +  | Const (@{const_name All}, _) $ t1 =>  (* similar to "Pure.all" *)
  14.104        let
  14.105          val (i, m, a) = interpret ctxt model args t1
  14.106        in
  14.107 @@ -1670,7 +1670,7 @@
  14.108        end
  14.109    | Const (@{const_name Ex}, _) =>
  14.110        SOME (interpret ctxt model args (eta_expand t 1))
  14.111 -  | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
  14.112 +  | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to Pure.eq *)
  14.113        let
  14.114          val (i1, m1, a1) = interpret ctxt model args t1
  14.115          val (i2, m2, a2) = interpret ctxt m1 a1 t2
  14.116 @@ -1715,7 +1715,7 @@
  14.117        (* this would make "undef" propagate, even for formulae like *)
  14.118        (* "True | undef":                                           *)
  14.119        (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
  14.120 -  | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
  14.121 +  | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to Pure.imp *)
  14.122        (* 3-valued logic *)
  14.123        let
  14.124          val (i1, m1, a1) = interpret ctxt model args t1
    15.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Mar 21 15:12:03 2014 +0100
    15.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Mar 21 20:33:56 2014 +0100
    15.3 @@ -435,7 +435,8 @@
    15.4               val ty = type_of a
    15.5               val (encoding, a) = remove_types encoding a
    15.6               val (encoding, b) = remove_types encoding b
    15.7 -             val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding 
    15.8 +             val (eq, encoding) =
    15.9 +              Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding 
   15.10           in
   15.11               (encoding, EqPrem (a, b, ty, eq))
   15.12           end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
    16.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 15:12:03 2014 +0100
    16.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 20:33:56 2014 +0100
    16.3 @@ -275,7 +275,7 @@
    16.4   @{const_name Quickcheck_Random.catch_match},
    16.5   @{const_name Quickcheck_Exhaustive.unknown},
    16.6   @{const_name Num.Bit0}, @{const_name Num.Bit1}
    16.7 - (*@{const_name "==>"}, @{const_name "=="}*)]
    16.8 + (*@{const_name Pure.imp}, @{const_name Pure.eq}*)]
    16.9  
   16.10  val forbidden_mutant_consts =
   16.11    [
    17.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 15:12:03 2014 +0100
    17.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 20:33:56 2014 +0100
    17.3 @@ -292,7 +292,7 @@
    17.4  
    17.5  subsection {* Known Constants *}
    17.6  
    17.7 -lemma "x \<equiv> all \<Longrightarrow> False"
    17.8 +lemma "x \<equiv> Pure.all \<Longrightarrow> False"
    17.9  nitpick [card = 1, expect = genuine]
   17.10  nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   17.11  nitpick [card = 6, expect = genuine]
   17.12 @@ -306,15 +306,15 @@
   17.13  nitpick [expect = genuine]
   17.14  oops
   17.15  
   17.16 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   17.17 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   17.18  nitpick [expect = none]
   17.19  by auto
   17.20  
   17.21 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   17.22 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   17.23  nitpick [expect = genuine]
   17.24  oops
   17.25  
   17.26 -lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
   17.27 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Pure.all P \<equiv> Pure.all (\<lambda>x. P (I x))"
   17.28  nitpick [expect = none]
   17.29  by auto
   17.30  
    18.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Mar 21 15:12:03 2014 +0100
    18.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Mar 21 20:33:56 2014 +0100
    18.3 @@ -326,7 +326,7 @@
    18.4  nitpick [expect = genuine]
    18.5  oops
    18.6  
    18.7 -lemma "(x \<equiv> all) \<Longrightarrow> False"
    18.8 +lemma "(x \<equiv> Pure.all) \<Longrightarrow> False"
    18.9  nitpick [expect = genuine]
   18.10  oops
   18.11  
    19.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 21 15:12:03 2014 +0100
    19.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 21 20:33:56 2014 +0100
    19.3 @@ -32,8 +32,8 @@
    19.4  
    19.5  fun unquantify t =
    19.6    let
    19.7 -    val (vs, Ts) = split_list (strip_qnt_vars "all" t);
    19.8 -    val body = strip_qnt_body "all" t;
    19.9 +    val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} t);
   19.10 +    val body = strip_qnt_body @{const_name Pure.all} t;
   19.11      val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
   19.12        (fn Free (v, _) => insert (op =) v | _ => I) body []))
   19.13    in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
    20.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Mar 21 15:12:03 2014 +0100
    20.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Mar 21 20:33:56 2014 +0100
    20.3 @@ -134,7 +134,7 @@
    20.4      val thy = Context.theory_of context
    20.5      val thms_to_be_added = (case (prop_of orig_thm) of
    20.6          (* case: eqvt-lemma is of the implicational form *)
    20.7 -        (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
    20.8 +        (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
    20.9            let
   20.10              val (pi,typi) = get_pi concl thy
   20.11            in
    21.1 --- a/src/HOL/Product_Type.thy	Fri Mar 21 15:12:03 2014 +0100
    21.2 +++ b/src/HOL/Product_Type.thy	Fri Mar 21 20:33:56 2014 +0100
    21.3 @@ -457,7 +457,7 @@
    21.4  ML {*
    21.5    (* replace parameters of product type by individual component parameters *)
    21.6    local (* filtering with exists_paired_all is an essential optimization *)
    21.7 -    fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
    21.8 +    fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
    21.9            can HOLogic.dest_prodT T orelse exists_paired_all t
   21.10        | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
   21.11        | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
    22.1 --- a/src/HOL/Prolog/prolog.ML	Fri Mar 21 15:12:03 2014 +0100
    22.2 +++ b/src/HOL/Prolog/prolog.ML	Fri Mar 21 20:33:56 2014 +0100
    22.3 @@ -13,9 +13,9 @@
    22.4      Const(@{const_name Trueprop},_)$t     => isD t
    22.5    | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
    22.6    | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
    22.7 -  | Const(   "==>",_)$l$r     => isG l andalso isD r
    22.8 +  | Const(@{const_name Pure.imp},_)$l$r     => isG l andalso isD r
    22.9    | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   22.10 -  | Const("all",_)$Abs(s,_,t) => isD t
   22.11 +  | Const(@{const_name Pure.all},_)$Abs(s,_,t) => isD t
   22.12    | Const(@{const_name HOL.disj},_)$_$_       => false
   22.13    | Const(@{const_name Ex} ,_)$_          => false
   22.14    | Const(@{const_name Not},_)$_          => false
   22.15 @@ -33,9 +33,9 @@
   22.16    | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
   22.17    | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
   22.18    | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   22.19 -  | Const(   "==>",_)$l$r     => isD l andalso isG r
   22.20 +  | Const(@{const_name Pure.imp},_)$l$r     => isD l andalso isG r
   22.21    | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   22.22 -  | Const("all",_)$Abs(_,_,t) => isG t
   22.23 +  | Const(@{const_name Pure.all},_)$Abs(_,_,t) => isG t
   22.24    | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
   22.25    | Const(@{const_name True},_)           => true
   22.26    | Const(@{const_name Not},_)$_          => false
   22.27 @@ -79,8 +79,8 @@
   22.28          |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   22.29          |   ap t                          =                         (0,false,t);
   22.30  (*
   22.31 -        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
   22.32 -        |   rep_goal (Const ("==>",_)$s$t)         =
   22.33 +        fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t
   22.34 +        |   rep_goal (Const (@{const_name Pure.imp},_)$s$t)         =
   22.35                          (case rep_goal t of (l,t) => (s::l,t))
   22.36          |   rep_goal t                             = ([]  ,t);
   22.37          val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
    23.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Mar 21 15:12:03 2014 +0100
    23.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Mar 21 20:33:56 2014 +0100
    23.3 @@ -320,7 +320,7 @@
    23.4      |> apfst the_single
    23.5  end
    23.6  
    23.7 -(*like strip_top_All_vars but for "all" instead of "All"*)
    23.8 +(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*)
    23.9  fun strip_top_all_vars acc t =
   23.10    if Logic.is_all t then
   23.11      let
    24.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 15:12:03 2014 +0100
    24.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 20:33:56 2014 +0100
    24.3 @@ -1670,7 +1670,7 @@
    24.4     (* @{const_name HOL.not_equal}, *)
    24.5     @{const_name HOL.False},
    24.6     @{const_name HOL.True},
    24.7 -   @{const_name "==>"}]
    24.8 +   @{const_name Pure.imp}]
    24.9  
   24.10  fun strip_qtfrs_tac ctxt =
   24.11    REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))
    25.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 15:12:03 2014 +0100
    25.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 20:33:56 2014 +0100
    25.3 @@ -404,8 +404,9 @@
    25.4  (* These are ignored anyway by the relevance filter (unless they appear in
    25.5     higher-order places) but not by the monomorphizer. *)
    25.6  val atp_logical_consts =
    25.7 -  [@{const_name Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
    25.8 -   @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    25.9 +  [@{const_name Pure.prop}, @{const_name Pure.conjunction},
   25.10 +   @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq},
   25.11 +   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   25.12     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   25.13  
   25.14  (* These are either simplified away by "Meson.presimplify" (most of the time) or
   25.15 @@ -1879,8 +1880,8 @@
   25.16    in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
   25.17  
   25.18  fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
   25.19 -  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
   25.20 -  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
   25.21 +  | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t
   25.22 +  | s_not_prop t = @{const Pure.imp} $ t $ @{prop False}
   25.23  
   25.24  fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
   25.25                         concl_t facts =
    26.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 15:12:03 2014 +0100
    26.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 20:33:56 2014 +0100
    26.3 @@ -46,7 +46,7 @@
    26.4  
    26.5  fun hhf_concl_conv cv ctxt ct =
    26.6    (case Thm.term_of ct of
    26.7 -    Const (@{const_name all}, _) $ Abs _ =>
    26.8 +    Const (@{const_name Pure.all}, _) $ Abs _ =>
    26.9      Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
   26.10    | _ => Conv.concl_conv ~1 cv ct);
   26.11  
    27.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Mar 21 15:12:03 2014 +0100
    27.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Mar 21 20:33:56 2014 +0100
    27.3 @@ -86,8 +86,8 @@
    27.4    | retype_free _ t = raise TERM ("retype_free", [t]);
    27.5  
    27.6  fun drop_all t =
    27.7 -  subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
    27.8 -    strip_qnt_body @{const_name all} t);
    27.9 +  subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
   27.10 +    strip_qnt_body @{const_name Pure.all} t);
   27.11  
   27.12  fun permute_args n t =
   27.13    list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
    28.1 --- a/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 15:12:03 2014 +0100
    28.2 +++ b/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 20:33:56 2014 +0100
    28.3 @@ -34,8 +34,8 @@
    28.4  
    28.5  fun process_eqn is_fixed spec rec_fns =
    28.6    let
    28.7 -    val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
    28.8 -    val body = strip_qnt_body "all" spec;
    28.9 +    val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec);
   28.10 +    val body = strip_qnt_body @{const_name Pure.all} spec;
   28.11      val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
   28.12        (fn Free (v, _) => insert (op =) v | _ => I) body []));
   28.13      val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
    29.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 15:12:03 2014 +0100
    29.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 20:33:56 2014 +0100
    29.3 @@ -434,7 +434,7 @@
    29.4    let
    29.5      fun prove_case_cong ((t, nchotomy), case_rewrites) =
    29.6        let
    29.7 -        val Const ("==>", _) $ tm $ _ = t;
    29.8 +        val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
    29.9          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
   29.10          val cert = cterm_of thy;
   29.11          val nchotomy' = nchotomy RS spec;
    30.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 15:12:03 2014 +0100
    30.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 20:33:56 2014 +0100
    30.3 @@ -280,8 +280,8 @@
    30.4  fun split_def ctxt check_head geq =
    30.5    let
    30.6      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
    30.7 -    val qs = Term.strip_qnt_vars "all" geq
    30.8 -    val imp = Term.strip_qnt_body "all" geq
    30.9 +    val qs = Term.strip_qnt_vars @{const_name Pure.all} geq
   30.10 +    val imp = Term.strip_qnt_body @{const_name Pure.all} geq
   30.11      val (gs, eq) = Logic.strip_horn imp
   30.12  
   30.13      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    31.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 15:12:03 2014 +0100
    31.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 20:33:56 2014 +0100
    31.3 @@ -40,7 +40,7 @@
    31.4  
    31.5  
    31.6  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    31.7 -fun dest_all_all (t as (Const ("all",_) $ _)) =
    31.8 +fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) =
    31.9    let
   31.10      val (v,b) = Logic.dest_all t |> apfst Free
   31.11      val (vs, b') = dest_all_all b
    32.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 15:12:03 2014 +0100
    32.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 20:33:56 2014 +0100
    32.3 @@ -547,11 +547,11 @@
    32.4  
    32.5  fun rename_to_tnames ctxt term =
    32.6    let
    32.7 -    fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t
    32.8 +    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
    32.9        | all_typs _ = []
   32.10  
   32.11 -    fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = 
   32.12 -        (Const ("all", T1) $ Abs (new_name, T2, rename t names)) 
   32.13 +    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   32.14 +        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   32.15        | rename t _ = t
   32.16  
   32.17      val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
    33.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 15:12:03 2014 +0100
    33.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 20:33:56 2014 +0100
    33.3 @@ -105,7 +105,7 @@
    33.4      try (fn () =>
    33.5        let val thy = theory_of_thm thA
    33.6            val tmA = concl_of thA
    33.7 -          val Const("==>",_) $ tmB $ _ = prop_of thB
    33.8 +          val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB
    33.9            val tenv =
   33.10              Pattern.first_order_match thy (tmB, tmA)
   33.11                                            (Vartab.empty, Vartab.empty) |> snd
   33.12 @@ -472,7 +472,7 @@
   33.13  
   33.14  (***** MESON PROOF PROCEDURE *****)
   33.15  
   33.16 -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   33.17 +fun rhyps (Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   33.18             As) = rhyps(phi, A::As)
   33.19    | rhyps (_, As) = As;
   33.20  
    34.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 15:12:03 2014 +0100
    34.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 20:33:56 2014 +0100
    34.3 @@ -242,7 +242,7 @@
    34.4      fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
    34.5        case t of
    34.6          (t1 as Const (s, _)) $ Abs (s', T, t') =>
    34.7 -        if s = @{const_name all} orelse s = @{const_name All} orelse
    34.8 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
    34.9             s = @{const_name Ex} then
   34.10            let
   34.11              val skolem = (pos = (s = @{const_name Ex}))
   34.12 @@ -254,7 +254,7 @@
   34.13          else
   34.14            t
   34.15        | (t1 as Const (s, _)) $ t2 $ t3 =>
   34.16 -        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
   34.17 +        if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then
   34.18            t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
   34.19          else if s = @{const_name HOL.conj} orelse
   34.20                  s = @{const_name HOL.disj} then
   34.21 @@ -275,13 +275,13 @@
   34.22    ct
   34.23    |> (case term_of ct of
   34.24          Const (s, _) $ Abs (s', _, _) =>
   34.25 -        if s = @{const_name all} orelse s = @{const_name All} orelse
   34.26 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
   34.27             s = @{const_name Ex} then
   34.28            Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
   34.29          else
   34.30            Conv.all_conv
   34.31        | Const (s, _) $ _ $ _ =>
   34.32 -        if s = @{const_name "==>"} orelse s = @{const_name implies} then
   34.33 +        if s = @{const_name Pure.imp} orelse s = @{const_name implies} then
   34.34            Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
   34.35          else if s = @{const_name conj} orelse s = @{const_name disj} then
   34.36            Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
    35.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 21 15:12:03 2014 +0100
    35.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 21 20:33:56 2014 +0100
    35.3 @@ -1062,7 +1062,7 @@
    35.4    end
    35.5  
    35.6  fun is_fixed_equation ctxt
    35.7 -                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
    35.8 +                      (Const (@{const_name Pure.eq}, _) $ Free (s, _) $ Const _) =
    35.9      Variable.is_fixed ctxt s
   35.10    | is_fixed_equation _ _ = false
   35.11  
    36.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 15:12:03 2014 +0100
    36.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 20:33:56 2014 +0100
    36.3 @@ -363,9 +363,9 @@
    36.4     "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
    36.5     well. *)
    36.6  val built_in_consts =
    36.7 -  [(@{const_name all}, 1),
    36.8 -   (@{const_name "=="}, 2),
    36.9 -   (@{const_name "==>"}, 2),
   36.10 +  [(@{const_name Pure.all}, 1),
   36.11 +   (@{const_name Pure.eq}, 2),
   36.12 +   (@{const_name Pure.imp}, 2),
   36.13     (@{const_name Pure.conjunction}, 2),
   36.14     (@{const_name Trueprop}, 1),
   36.15     (@{const_name Not}, 1),
   36.16 @@ -973,7 +973,7 @@
   36.17        fold (fn (z as ((s, _), T)) => fn t' =>
   36.18                 Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
   36.19             (take (length zs' - length zs) zs')
   36.20 -    fun aux zs (@{const "==>"} $ t1 $ t2) =
   36.21 +    fun aux zs (@{const Pure.imp} $ t1 $ t2) =
   36.22          let val zs' = Term.add_vars t1 zs in
   36.23            close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
   36.24          end
   36.25 @@ -1178,7 +1178,7 @@
   36.26    | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   36.27    | loose_bvar1_count _ = 0
   36.28  
   36.29 -fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) =
   36.30 +fun s_betapply _ (t1 as Const (@{const_name Pure.eq}, _) $ t1', t2) =
   36.31      if t1' aconv t2 then @{prop True} else t1 $ t2
   36.32    | s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) =
   36.33      if t1' aconv t2 then @{term True} else t1 $ t2
   36.34 @@ -1422,8 +1422,8 @@
   36.35     simplification rules (equational specifications). *)
   36.36  fun term_under_def t =
   36.37    case t of
   36.38 -    @{const "==>"} $ _ $ t2 => term_under_def t2
   36.39 -  | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
   36.40 +    @{const Pure.imp} $ _ $ t2 => term_under_def t2
   36.41 +  | Const (@{const_name Pure.eq}, _) $ t1 $ _ => term_under_def t1
   36.42    | @{const Trueprop} $ t1 => term_under_def t1
   36.43    | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
   36.44    | Abs (_, _, t') => term_under_def t'
   36.45 @@ -1448,7 +1448,7 @@
   36.46        | aux _ _ = NONE
   36.47      val (lhs, rhs) =
   36.48        case t of
   36.49 -        Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
   36.50 +        Const (@{const_name Pure.eq}, _) $ t1 $ t2 => (t1, t2)
   36.51        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
   36.52          (t1, t2)
   36.53        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
   36.54 @@ -1527,9 +1527,9 @@
   36.55  
   36.56  fun lhs_of_equation t =
   36.57    case t of
   36.58 -    Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   36.59 -  | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
   36.60 -  | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
   36.61 +    Const (@{const_name Pure.all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   36.62 +  | Const (@{const_name Pure.eq}, _) $ t1 $ _ => SOME t1
   36.63 +  | @{const Pure.imp} $ _ $ t2 => lhs_of_equation t2
   36.64    | @{const Trueprop} $ t1 => lhs_of_equation t1
   36.65    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   36.66    | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
   36.67 @@ -1947,7 +1947,7 @@
   36.68            @{const Trueprop} $ extensional_equal j T t1 t2
   36.69          | @{const Trueprop} $ t' =>
   36.70            @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
   36.71 -        | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   36.72 +        | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   36.73            @{const Trueprop} $ extensional_equal j T t1 t2
   36.74          | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
   36.75                           quote (Syntax.string_of_term ctxt t) ^ ".");
    37.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 21 15:12:03 2014 +0100
    37.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 21 20:33:56 2014 +0100
    37.3 @@ -844,8 +844,8 @@
    37.4              if not (could_exist_alpha_subtype alpha_T T) then
    37.5                (mtype_for T, accum)
    37.6              else case s of
    37.7 -              @{const_name all} => do_all T accum
    37.8 -            | @{const_name "=="} => do_equals T accum
    37.9 +              @{const_name Pure.all} => do_all T accum
   37.10 +            | @{const_name Pure.eq} => do_equals T accum
   37.11              | @{const_name All} => do_all T accum
   37.12              | @{const_name Ex} =>
   37.13                let val set_T = domain_type T in
   37.14 @@ -1057,9 +1057,9 @@
   37.15                              " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   37.16                              " : o\<^sup>" ^ string_for_sign sn ^ "?");
   37.17          case t of
   37.18 -          Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
   37.19 +          Const (s as @{const_name Pure.all}, _) $ Abs (_, T1, t1) =>
   37.20            do_quantifier s T1 t1
   37.21 -        | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
   37.22 +        | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => do_equals t1 t2
   37.23          | @{const Trueprop} $ t1 => do_formula sn t1 accum
   37.24          | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
   37.25            do_quantifier s T1 t1
   37.26 @@ -1076,7 +1076,7 @@
   37.27            do_formula sn (betapply (t2, t1)) accum
   37.28          | @{const Pure.conjunction} $ t1 $ t2 =>
   37.29            do_connect meta_conj_spec false t1 t2 accum
   37.30 -        | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   37.31 +        | @{const Pure.imp} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   37.32          | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
   37.33          | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
   37.34          | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
   37.35 @@ -1122,11 +1122,11 @@
   37.36        and do_implies t1 t2 = do_term t1 #> do_formula t2
   37.37        and do_formula t accum =
   37.38          case t of
   37.39 -          Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   37.40 +          Const (@{const_name Pure.all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   37.41          | @{const Trueprop} $ t1 => do_formula t1 accum
   37.42 -        | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   37.43 +        | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
   37.44            consider_general_equals mdata true t1 t2 accum
   37.45 -        | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
   37.46 +        | @{const Pure.imp} $ t1 $ t2 => do_implies t1 t2 accum
   37.47          | @{const Pure.conjunction} $ t1 $ t2 =>
   37.48            fold (do_formula) [t1, t2] accum
   37.49          | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
    38.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Mar 21 15:12:03 2014 +0100
    38.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Mar 21 20:33:56 2014 +0100
    38.3 @@ -474,12 +474,12 @@
    38.4            | k => sub (eta_expand Ts t k)
    38.5        in
    38.6          case strip_comb t of
    38.7 -          (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
    38.8 +          (Const (@{const_name Pure.all}, _), [Abs (s, T, t1)]) =>
    38.9            do_quantifier All s T t1
   38.10 -        | (t0 as Const (@{const_name all}, _), [t1]) =>
   38.11 +        | (t0 as Const (@{const_name Pure.all}, _), [t1]) =>
   38.12            sub' (t0 $ eta_expand Ts t1 1)
   38.13 -        | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
   38.14 -        | (Const (@{const_name "==>"}, _), [t1, t2]) =>
   38.15 +        | (Const (@{const_name Pure.eq}, T), [t1, t2]) => sub_equals T t1 t2
   38.16 +        | (Const (@{const_name Pure.imp}, _), [t1, t2]) =>
   38.17            Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
   38.18          | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
   38.19            Op2 (And, prop_T, Any, sub' t1, sub' t2)
    39.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 15:12:03 2014 +0100
    39.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 20:33:56 2014 +0100
    39.3 @@ -36,9 +36,9 @@
    39.4  
    39.5  val may_use_binary_ints =
    39.6    let
    39.7 -    fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
    39.8 +    fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) =
    39.9          aux def t1 andalso aux false t2
   39.10 -      | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
   39.11 +      | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def t2
   39.12        | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
   39.13          aux def t1 andalso aux false t2
   39.14        | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
   39.15 @@ -145,7 +145,7 @@
   39.16        case t of
   39.17          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   39.18        | Const (s0, _) $ t1 $ _ =>
   39.19 -        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
   39.20 +        if s0 = @{const_name Pure.eq} orelse s0 = @{const_name HOL.eq} then
   39.21            let
   39.22              val (t', args) = strip_comb t1
   39.23              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   39.24 @@ -187,12 +187,12 @@
   39.25        end
   39.26      and do_term new_Ts old_Ts polar t =
   39.27        case t of
   39.28 -        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   39.29 +        Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   39.30          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   39.31 -      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
   39.32 +      | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 =>
   39.33          do_equals new_Ts old_Ts s0 T0 t1 t2
   39.34 -      | @{const "==>"} $ t1 $ t2 =>
   39.35 -        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   39.36 +      | @{const Pure.imp} $ t1 $ t2 =>
   39.37 +        @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   39.38          $ do_term new_Ts old_Ts polar t2
   39.39        | @{const Pure.conjunction} $ t1 $ t2 =>
   39.40          @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
   39.41 @@ -334,9 +334,9 @@
   39.42      val k = maxidx_of_term t + 1
   39.43      fun do_term Ts def t args seen =
   39.44        case t of
   39.45 -        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
   39.46 +        (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 =>
   39.47          do_eq_or_imp Ts true def t0 t1 t2 seen
   39.48 -      | (t0 as @{const "==>"}) $ t1 $ t2 =>
   39.49 +      | (t0 as @{const Pure.imp}) $ t1 $ t2 =>
   39.50          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   39.51        | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   39.52          do_eq_or_imp Ts true def t0 t1 t2 seen
   39.53 @@ -401,9 +401,9 @@
   39.54      val num_occs_of_var =
   39.55        fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   39.56                      | _ => I) t (K 0)
   39.57 -    fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
   39.58 +    fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) =
   39.59          aux_eq Ts careful true t0 t1 t2
   39.60 -      | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
   39.61 +      | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) =
   39.62          t0 $ aux Ts false t1 $ aux Ts careful t2
   39.63        | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
   39.64          aux_eq Ts careful true t0 t1 t2
   39.65 @@ -455,22 +455,22 @@
   39.66  
   39.67  (** Destruction of universal and existential equalities **)
   39.68  
   39.69 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
   39.70 +fun curry_assms (@{const Pure.imp} $ (@{const Trueprop}
   39.71                                     $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
   39.72      curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   39.73 -  | curry_assms (@{const "==>"} $ t1 $ t2) =
   39.74 -    @{const "==>"} $ curry_assms t1 $ curry_assms t2
   39.75 +  | curry_assms (@{const Pure.imp} $ t1 $ t2) =
   39.76 +    @{const Pure.imp} $ curry_assms t1 $ curry_assms t2
   39.77    | curry_assms t = t
   39.78  
   39.79  val destroy_universal_equalities =
   39.80    let
   39.81      fun aux prems zs t =
   39.82        case t of
   39.83 -        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
   39.84 +        @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2
   39.85        | _ => Logic.list_implies (rev prems, t)
   39.86      and aux_implies prems zs t1 t2 =
   39.87        case t1 of
   39.88 -        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   39.89 +        Const (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   39.90        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
   39.91          aux_eq prems zs z t' t1 t2
   39.92        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
   39.93 @@ -591,10 +591,10 @@
   39.94                               not (is_higher_order_type abs_T)) polar t)
   39.95        in
   39.96          case t of
   39.97 -          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   39.98 +          Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   39.99            do_quantifier s0 T0 s1 T1 t1
  39.100 -        | @{const "==>"} $ t1 $ t2 =>
  39.101 -          @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
  39.102 +        | @{const Pure.imp} $ t1 $ t2 =>
  39.103 +          @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1
  39.104            $ aux ss Ts js skolemizable polar t2
  39.105          | @{const Pure.conjunction} $ t1 $ t2 =>
  39.106            @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
  39.107 @@ -654,7 +654,7 @@
  39.108  
  39.109  (** Function specialization **)
  39.110  
  39.111 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
  39.112 +fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2
  39.113    | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
  39.114    | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
  39.115      snd (strip_comb t1)
  39.116 @@ -866,7 +866,7 @@
  39.117        if exists_subterm (curry (op aconv) u) def then NONE else SOME u
  39.118    in
  39.119      case t of
  39.120 -      Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def
  39.121 +      Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def
  39.122      | @{const Trueprop}
  39.123        $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
  39.124        do_equals u def
  39.125 @@ -918,7 +918,7 @@
  39.126      and add_def_axiom depth = add_axiom fst apfst true depth
  39.127      and add_nondef_axiom depth = add_axiom snd apsnd false depth
  39.128      and add_maybe_def_axiom depth t =
  39.129 -      (if head_of t <> @{const "==>"} then add_def_axiom
  39.130 +      (if head_of t <> @{const Pure.imp} then add_def_axiom
  39.131         else add_nondef_axiom) depth t
  39.132      and add_eq_axiom depth t =
  39.133        (if is_constr_pattern_formula ctxt t then add_def_axiom
    40.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 21 15:12:03 2014 +0100
    40.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 21 20:33:56 2014 +0100
    40.3 @@ -307,7 +307,8 @@
    40.4  
    40.5  fun imp_prems_conv cv ct =
    40.6    (case Thm.term_of ct of
    40.7 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    40.8 +    Const (@{const_name Pure.imp}, _) $ _ $ _ =>
    40.9 +      Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   40.10    | _ => Conv.all_conv ct)
   40.11  
   40.12  fun preprocess_intro thy rule =
    41.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 15:12:03 2014 +0100
    41.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 20:33:56 2014 +0100
    41.3 @@ -460,14 +460,14 @@
    41.4  
    41.5  (* general syntactic functions *)
    41.6  
    41.7 -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    41.8 +fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = true
    41.9    | is_equationlike_term
   41.10        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
   41.11    | is_equationlike_term _ = false
   41.12  
   41.13  val is_equationlike = is_equationlike_term o prop_of
   41.14  
   41.15 -fun is_pred_equation_term (Const ("==", _) $ u $ v) =
   41.16 +fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) =
   41.17        (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
   41.18    | is_pred_equation_term _ = false
   41.19  
   41.20 @@ -620,7 +620,7 @@
   41.21  (*
   41.22  fun equals_conv lhs_cv rhs_cv ct =
   41.23    case Thm.term_of ct of
   41.24 -    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
   41.25 +    Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct
   41.26    | _ => error "equals_conv"
   41.27  *)
   41.28  
   41.29 @@ -973,7 +973,8 @@
   41.30  
   41.31  fun imp_prems_conv cv ct =
   41.32    (case Thm.term_of ct of
   41.33 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   41.34 +    Const (@{const_name Pure.imp}, _) $ _ $ _ =>
   41.35 +      Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   41.36    | _ => Conv.all_conv ct)
   41.37  
   41.38  
    42.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 21 15:12:03 2014 +0100
    42.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 21 20:33:56 2014 +0100
    42.3 @@ -84,7 +84,7 @@
    42.4  
    42.5  val is_introlike = is_introlike_term o prop_of
    42.6  
    42.7 -fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
    42.8 +fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) =
    42.9        (case strip_comb u of
   42.10          (Const (_, T), args) =>
   42.11            if (length (binder_types T) = length args) then
   42.12 @@ -98,7 +98,7 @@
   42.13  val check_equation_format = check_equation_format_term o prop_of
   42.14  
   42.15  
   42.16 -fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
   42.17 +fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u)
   42.18    | defining_term_of_equation_term t =
   42.19        raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
   42.20  
   42.21 @@ -224,8 +224,8 @@
   42.22    end
   42.23  
   42.24  val logic_operator_names =
   42.25 -  [@{const_name "=="},
   42.26 -   @{const_name "==>"},
   42.27 +  [@{const_name Pure.eq},
   42.28 +   @{const_name Pure.imp},
   42.29     @{const_name Trueprop},
   42.30     @{const_name Not},
   42.31     @{const_name HOL.eq},
    43.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Mar 21 15:12:03 2014 +0100
    43.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Mar 21 20:33:56 2014 +0100
    43.3 @@ -795,7 +795,7 @@
    43.4  
    43.5  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    43.6   let 
    43.7 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    43.8 +   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
    43.9     fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
   43.10     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   43.11     val p' = fold_rev gen ts p
    44.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 15:12:03 2014 +0100
    44.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 20:33:56 2014 +0100
    44.3 @@ -52,7 +52,7 @@
    44.4    (case Thm.prop_of thm of
    44.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    44.6        norm_def (thm RS @{thm fun_cong})
    44.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    44.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
    44.9        norm_def (thm RS @{thm meta_eq_to_obj_eq})
   44.10    | _ => thm)
   44.11  
   44.12 @@ -61,20 +61,20 @@
   44.13  
   44.14  fun atomize_conv ctxt ct =
   44.15    (case Thm.term_of ct of
   44.16 -    @{const "==>"} $ _ $ _ =>
   44.17 +    @{const Pure.imp} $ _ $ _ =>
   44.18        Conv.binop_conv (atomize_conv ctxt) then_conv
   44.19        Conv.rewr_conv @{thm atomize_imp}
   44.20 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
   44.21 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   44.22        Conv.binop_conv (atomize_conv ctxt) then_conv
   44.23        Conv.rewr_conv @{thm atomize_eq}
   44.24 -  | Const (@{const_name all}, _) $ Abs _ =>
   44.25 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
   44.26        Conv.binder_conv (atomize_conv o snd) ctxt then_conv
   44.27        Conv.rewr_conv @{thm atomize_all}
   44.28    | _ => Conv.all_conv) ct
   44.29  
   44.30  val setup_atomize =
   44.31 -  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
   44.32 -    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
   44.33 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
   44.34 +    @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
   44.35  
   44.36  
   44.37  (** unfold special quantifiers **)
    45.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Fri Mar 21 15:12:03 2014 +0100
    45.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Fri Mar 21 20:33:56 2014 +0100
    45.3 @@ -188,7 +188,7 @@
    45.4      @{const Trueprop} $ _ => Thm.dest_arg ct
    45.5    | _ => raise CTERM ("not a property", [ct]))
    45.6  
    45.7 -val equals = mk_const_pat @{theory} @{const_name "=="} destT1
    45.8 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
    45.9  fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
   45.10  
   45.11  val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    46.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Mar 21 15:12:03 2014 +0100
    46.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Mar 21 20:33:56 2014 +0100
    46.3 @@ -614,7 +614,7 @@
    46.4  (* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
    46.5  local
    46.6    val forall =
    46.7 -    SMT_Utils.mk_const_pat @{theory} @{const_name all}
    46.8 +    SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all}
    46.9        (SMT_Utils.destT1 o SMT_Utils.destT1)
   46.10    fun mk_forall cv ct =
   46.11      Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
    47.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 15:12:03 2014 +0100
    47.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 20:33:56 2014 +0100
    47.3 @@ -199,7 +199,7 @@
    47.4      and abstr (dcvs as (d, cvs)) ct =
    47.5        (case Thm.term_of ct of
    47.6          @{const Trueprop} $ _ => abstr1 dcvs ct
    47.7 -      | @{const "==>"} $ _ $ _ => abstr2 dcvs ct
    47.8 +      | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
    47.9        | @{const True} => pair ct
   47.10        | @{const False} => pair ct
   47.11        | @{const Not} $ _ => abstr1 dcvs ct
   47.12 @@ -229,7 +229,7 @@
   47.13              | _ => fresh_abstraction dcvs ct cx)))
   47.14    in abstr (depth, []) end
   47.15  
   47.16 -val cimp = Thm.cterm_of @{theory} @{const "==>"}
   47.17 +val cimp = Thm.cterm_of @{theory} @{const Pure.imp}
   47.18  
   47.19  fun deepen depth f x =
   47.20    if depth = 0 then f depth x
    48.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 15:12:03 2014 +0100
    48.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 20:33:56 2014 +0100
    48.3 @@ -48,7 +48,7 @@
    48.4    (case Thm.prop_of thm of
    48.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    48.6        norm_def (thm RS @{thm fun_cong})
    48.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    48.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    48.9    | _ => thm)
   48.10  
   48.11  
   48.12 @@ -56,17 +56,17 @@
   48.13  
   48.14  fun atomize_conv ctxt ct =
   48.15    (case Thm.term_of ct of
   48.16 -    @{const "==>"} $ _ $ _ =>
   48.17 +    @{const Pure.imp} $ _ $ _ =>
   48.18        Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
   48.19 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
   48.20 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   48.21        Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
   48.22 -  | Const (@{const_name all}, _) $ Abs _ =>
   48.23 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
   48.24        Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
   48.25    | _ => Conv.all_conv) ct
   48.26  
   48.27  val setup_atomize =
   48.28 -  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
   48.29 -    @{const_name all}, @{const_name Trueprop}]
   48.30 +  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
   48.31 +    @{const_name Pure.all}, @{const_name Trueprop}]
   48.32  
   48.33  
   48.34  (** unfold special quantifiers **)
    49.1 --- a/src/HOL/Tools/SMT2/smt2_util.ML	Fri Mar 21 15:12:03 2014 +0100
    49.2 +++ b/src/HOL/Tools/SMT2/smt2_util.ML	Fri Mar 21 20:33:56 2014 +0100
    49.3 @@ -185,7 +185,7 @@
    49.4      @{const Trueprop} $ _ => Thm.dest_arg ct
    49.5    | _ => raise CTERM ("not a property", [ct]))
    49.6  
    49.7 -val equals = mk_const_pat @{theory} @{const_name "=="} destT1
    49.8 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
    49.9  fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
   49.10  
   49.11  val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    50.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 15:12:03 2014 +0100
    50.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 20:33:56 2014 +0100
    50.3 @@ -463,7 +463,7 @@
    50.4      val match = Sign.typ_match (Proof_Context.theory_of ctxt)
    50.5  
    50.6      val t' = singleton (Variable.polymorphic ctxt) t
    50.7 -    val patTs = map snd (Term.strip_qnt_vars @{const_name all} t')
    50.8 +    val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
    50.9      val objTs = map (the o Symtab.lookup env) bounds
   50.10      val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   50.11    in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
   50.12 @@ -501,7 +501,7 @@
   50.13      SOME (tyenv, _) => subst_of tyenv
   50.14    | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
   50.15  
   50.16 -fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) =
   50.17 +fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
   50.18        dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
   50.19    | dest_all i t = (i, t)
   50.20  
   50.21 @@ -517,7 +517,7 @@
   50.22      | SOME subst =>
   50.23          let
   50.24            val applyT = Same.commit (substTs_same subst)
   50.25 -          val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'')
   50.26 +          val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
   50.27          in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
   50.28    end
   50.29  
    51.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Fri Mar 21 15:12:03 2014 +0100
    51.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Fri Mar 21 20:33:56 2014 +0100
    51.3 @@ -14,7 +14,7 @@
    51.4  structure Z3_New_Replay: Z3_NEW_REPLAY =
    51.5  struct
    51.6  
    51.7 -fun params_of t = Term.strip_qnt_vars @{const_name all} t
    51.8 +fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t
    51.9  
   51.10  fun varify ctxt thm =
   51.11    let
   51.12 @@ -32,7 +32,7 @@
   51.13      fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
   51.14    in (ctxt', Symtab.make (map2 mk nTs ns)) end
   51.15  
   51.16 -fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
   51.17 +fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
   51.18        Term.betapply (a, Thm.term_of ct)
   51.19    | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
   51.20  
    52.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 21 15:12:03 2014 +0100
    52.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 21 20:33:56 2014 +0100
    52.3 @@ -85,8 +85,8 @@
    52.4  
    52.5  fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    52.6  fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    52.7 -  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    52.8 -  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    52.9 +  | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
   52.10 +  | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   52.11    | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   52.12    | is_rec_def _ = false
   52.13  
   52.14 @@ -260,13 +260,13 @@
   52.15        else
   52.16          Interesting
   52.17      fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
   52.18 -      | interest_of_prop Ts (@{const "==>"} $ t $ u) =
   52.19 +      | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
   52.20          combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
   52.21 -      | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   52.22 +      | interest_of_prop Ts (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
   52.23          if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
   52.24 -      | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   52.25 +      | interest_of_prop Ts ((t as Const (@{const_name Pure.all}, _)) $ u) =
   52.26          interest_of_prop Ts (t $ eta_expand Ts u 1)
   52.27 -      | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   52.28 +      | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
   52.29          combine_interests (interest_of_bool t) (interest_of_bool u)
   52.30        | interest_of_prop _ _ = Deal_Breaker
   52.31      val t = prop_of th
   52.32 @@ -351,7 +351,7 @@
   52.33    | normalize_eq (@{const Trueprop} $ (t as @{const Not}
   52.34          $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   52.35      if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
   52.36 -  | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   52.37 +  | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
   52.38      (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
   52.39      |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
   52.40    | normalize_eq t = t
    53.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Mar 21 15:12:03 2014 +0100
    53.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Mar 21 20:33:56 2014 +0100
    53.3 @@ -187,9 +187,9 @@
    53.4        if T = HOLogic.boolT then do_formula else do_term ext_arg
    53.5      and do_formula t =
    53.6        (case t of
    53.7 -        Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
    53.8 -      | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
    53.9 -      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   53.10 +        Const (@{const_name Pure.all}, _) $ Abs (_, _, t') => do_formula t'
   53.11 +      | @{const Pure.imp} $ t1 $ t2 => do_formula t1 #> do_formula t2
   53.12 +      | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   53.13          do_term_or_formula false T t1 #> do_term_or_formula true T t2
   53.14        | @{const Trueprop} $ t1 => do_formula t1
   53.15        | @{const False} => I
    54.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 21 15:12:03 2014 +0100
    54.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 21 20:33:56 2014 +0100
    54.3 @@ -77,10 +77,10 @@
    54.4      fun do_formula pos t =
    54.5        (case (pos, t) of
    54.6          (_, @{const Trueprop} $ t1) => do_formula pos t1
    54.7 -      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t'
    54.8 +      | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t'
    54.9        | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
   54.10        | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
   54.11 -      | (_, @{const "==>"} $ t1 $ t2) =>
   54.12 +      | (_, @{const Pure.imp} $ t1 $ t2) =>
   54.13          do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
   54.14        | (_, @{const HOL.implies} $ t1 $ t2) =>
   54.15          do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
   54.16 @@ -88,7 +88,7 @@
   54.17        | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   54.18        | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   54.19        | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   54.20 -      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   54.21 +      | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2
   54.22        | _ => false)
   54.23    in do_formula true end
   54.24  
    55.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Mar 21 15:12:03 2014 +0100
    55.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 21 20:33:56 2014 +0100
    55.3 @@ -63,7 +63,7 @@
    55.4     
    55.5  val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
    55.6  fun mk_meta_eq r = case concl_of r of
    55.7 -     Const("==",_)$_$_ => r
    55.8 +     Const(@{const_name Pure.eq},_)$_$_ => r
    55.9    |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
   55.10    |   _ => r RS P_imp_P_eq_True
   55.11  
    56.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Mar 21 15:12:03 2014 +0100
    56.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Mar 21 20:33:56 2014 +0100
    56.3 @@ -293,7 +293,7 @@
    56.4  fun GEN v th =
    56.5     let val gth = Thm.forall_intr v th
    56.6         val thy = Thm.theory_of_thm gth
    56.7 -       val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
    56.8 +       val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
    56.9         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   56.10         val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
   56.11         val allI2 = Drule.instantiate_normalize (certify thy theta) allI
   56.12 @@ -441,21 +441,22 @@
   56.13  
   56.14  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   56.15  fun is_cong thm =
   56.16 -  case (Thm.prop_of thm)
   56.17 -     of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
   56.18 -         (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
   56.19 -      | _ => true;
   56.20 +  case (Thm.prop_of thm) of
   56.21 +    (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
   56.22 +      (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) =>
   56.23 +        false
   56.24 +  | _ => true;
   56.25  
   56.26  
   56.27 -fun dest_equal(Const ("==",_) $
   56.28 +fun dest_equal(Const (@{const_name Pure.eq},_) $
   56.29                 (Const (@{const_name Trueprop},_) $ lhs)
   56.30                 $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
   56.31 -  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   56.32 +  | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
   56.33    | dest_equal tm = USyntax.dest_eq tm;
   56.34  
   56.35  fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   56.36  
   56.37 -fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
   56.38 +fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
   56.39    | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
   56.40  
   56.41  val is_all = can (dest_all []);
   56.42 @@ -468,10 +469,10 @@
   56.43          end
   56.44     else ([], fm, used);
   56.45  
   56.46 -fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   56.47 +fun break_all(Const(@{const_name Pure.all},_) $ Abs (_,_,body)) = body
   56.48    | break_all _ = raise RULES_ERR "break_all" "not a !!";
   56.49  
   56.50 -fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
   56.51 +fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
   56.52       let val (L,core) = list_break_all body
   56.53       in ((s,ty)::L, core)
   56.54       end
   56.55 @@ -725,7 +726,7 @@
   56.56  
   56.57               fun eliminate thm =
   56.58                 case Thm.prop_of thm
   56.59 -               of Const("==>",_) $ imp $ _ =>
   56.60 +               of Const(@{const_name Pure.imp},_) $ imp $ _ =>
   56.61                     eliminate
   56.62                      (if not(is_all imp)
   56.63                       then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
   56.64 @@ -740,7 +741,8 @@
   56.65                val cntxt = rev (Simplifier.prems_of ctxt)
   56.66                val dummy = print_thms ctxt "cntxt:" cntxt
   56.67                val thy = Thm.theory_of_thm thm
   56.68 -              val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
   56.69 +              val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
   56.70 +                Thm.prop_of thm
   56.71                fun genl tm = let val vlist = subtract (op aconv) globals
   56.72                                             (Misc_Legacy.add_term_frees(tm,[]))
   56.73                              in fold_rev Forall vlist tm
    57.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Mar 21 15:12:03 2014 +0100
    57.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Fri Mar 21 20:33:56 2014 +0100
    57.3 @@ -357,7 +357,7 @@
    57.4  (*For Isabelle, the lhs of a definition must be a constant.*)
    57.5  fun const_def sign (c, Ty, rhs) =
    57.6    singleton (Syntax.check_terms (Proof_Context.init_global sign))
    57.7 -    (Const("==",dummyT) $ Const(c,Ty) $ rhs);
    57.8 +    (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
    57.9  
   57.10  (*Make all TVars available for instantiation by adding a ? to the front*)
   57.11  fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
    58.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri Mar 21 15:12:03 2014 +0100
    58.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Mar 21 20:33:56 2014 +0100
    58.3 @@ -193,7 +193,7 @@
    58.4      val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    58.5      val t = Thm.term_of ct;
    58.6      val T = fastype_of t;
    58.7 -    val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
    58.8 +    val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
    58.9    in case value ctxt t
   58.10     of NONE => Thm.reflexive ct
   58.11      | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
   58.12 @@ -206,9 +206,9 @@
   58.13  
   58.14  fun static_conv ctxt consts Ts =
   58.15    let
   58.16 -    val eqs = "==" :: @{const_name HOL.eq} ::
   58.17 +    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
   58.18        map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
   58.19 -        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
   58.20 +        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
   58.21      val value = static_value ctxt consts Ts;
   58.22      val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
   58.23    in
    59.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 21 15:12:03 2014 +0100
    59.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 21 20:33:56 2014 +0100
    59.3 @@ -258,7 +258,7 @@
    59.4        handle THM _ => thm RS @{thm le_boolD}
    59.5    in
    59.6      (case concl_of thm of
    59.7 -      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
    59.8 +      Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
    59.9      | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
   59.10      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   59.11        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    60.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 15:12:03 2014 +0100
    60.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 20:33:56 2014 +0100
    60.3 @@ -31,20 +31,21 @@
    60.4  
    60.5  val pred_of = fst o dest_Const o head_of;
    60.6  
    60.7 -fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    60.8 +fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) =
    60.9        let val (s', names') = (case names of
   60.10            [] => (singleton (Name.variant_list used) s, [])
   60.11          | name :: names' => (name, names'))
   60.12        in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   60.13 -  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
   60.14 +  | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) =
   60.15        t $ strip_all' used names Q
   60.16    | strip_all' _ _ t = t;
   60.17  
   60.18  fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
   60.19  
   60.20 -fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
   60.21 +fun strip_one name
   60.22 +    (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) =
   60.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
   60.24 -  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
   60.25 +  | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q);
   60.26  
   60.27  fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
   60.28       (case strip_type T of
   60.29 @@ -145,8 +146,8 @@
   60.30  
   60.31      val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
   60.32  
   60.33 -    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   60.34 -      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   60.35 +    fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P
   60.36 +      | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
   60.37        | is_meta (Const (@{const_name Trueprop}, _) $ t) =
   60.38            (case head_of t of
   60.39              Const (s, _) => can (Inductive.the_inductive ctxt) s
    61.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Mar 21 15:12:03 2014 +0100
    61.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 21 20:33:56 2014 +0100
    61.3 @@ -50,7 +50,7 @@
    61.4                          addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
    61.5                      in
    61.6                        SOME (Goal.prove ctxt [] []
    61.7 -                        (Const ("==", T --> T --> propT) $ S $ S')
    61.8 +                        (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
    61.9                          (K (EVERY
   61.10                            [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
   61.11                             rtac subsetI 1, dtac CollectD 1, simp,
    62.1 --- a/src/HOL/Tools/record.ML	Fri Mar 21 15:12:03 2014 +0100
    62.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 21 20:33:56 2014 +0100
    62.3 @@ -1287,7 +1287,7 @@
    62.4      (fn ctxt => fn t =>
    62.5        (case t of
    62.6          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
    62.7 -          if quantifier = @{const_name all} orelse
    62.8 +          if quantifier = @{const_name Pure.all} orelse
    62.9              quantifier = @{const_name All} orelse
   62.10              quantifier = @{const_name Ex}
   62.11            then
   62.12 @@ -1301,7 +1301,7 @@
   62.13                      | SOME (all_thm, All_thm, Ex_thm, _) =>
   62.14                          SOME
   62.15                            (case quantifier of
   62.16 -                            @{const_name all} => all_thm
   62.17 +                            @{const_name Pure.all} => all_thm
   62.18                            | @{const_name All} => All_thm RS @{thm eq_reflection}
   62.19                            | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
   62.20                            | _ => raise Fail "split_simproc"))
   62.21 @@ -1368,8 +1368,8 @@
   62.22  
   62.23      val has_rec = exists_Const
   62.24        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   62.25 -          (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
   62.26 -          is_recT T
   62.27 +          (s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex})
   62.28 +            andalso is_recT T
   62.29          | _ => false);
   62.30  
   62.31      fun mk_split_free_tac free induct_thm i =
   62.32 @@ -1418,10 +1418,10 @@
   62.33  
   62.34      val has_rec = exists_Const
   62.35        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   62.36 -          (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
   62.37 +          (s = @{const_name Pure.all} orelse s = @{const_name All}) andalso is_recT T
   62.38          | _ => false);
   62.39  
   62.40 -    fun is_all (Const (@{const_name all}, _) $ _) = ~1
   62.41 +    fun is_all (Const (@{const_name Pure.all}, _) $ _) = ~1
   62.42        | is_all (Const (@{const_name All}, _) $ _) = ~1
   62.43        | is_all _ = 0;
   62.44    in
    63.1 --- a/src/HOL/Tools/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
    63.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
    63.3 @@ -43,7 +43,7 @@
    63.4  
    63.5  fun mk_eq th = case concl_of th
    63.6    (*expects Trueprop if not == *)
    63.7 -  of Const (@{const_name "=="},_) $ _ $ _ => th
    63.8 +  of Const (@{const_name Pure.eq},_) $ _ $ _ => th
    63.9     | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
   63.10     | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
   63.11     | _ => th RS @{thm Eq_TrueI}
    64.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Mar 21 15:12:03 2014 +0100
    64.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Mar 21 20:33:56 2014 +0100
    64.3 @@ -325,7 +325,7 @@
    64.4  refute [expect = genuine]
    64.5  oops
    64.6  
    64.7 -lemma "(x == all) \<Longrightarrow> False"
    64.8 +lemma "(x == Pure.all) \<Longrightarrow> False"
    64.9  refute [expect = genuine]
   64.10  oops
   64.11  
    65.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 15:12:03 2014 +0100
    65.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 20:33:56 2014 +0100
    65.3 @@ -100,7 +100,7 @@
    65.4        | fm t = replace t
    65.5      (*entry point, and abstraction of a meta-formula*)
    65.6      fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
    65.7 -      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    65.8 +      | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q)  = c $ (mt p) $ (mt q)
    65.9        | mt t = fm t  (*it might be a formula*)
   65.10    in (Logic.list_all (params, mt body), !pairs) end;
   65.11  
    66.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Mar 21 15:12:03 2014 +0100
    66.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 21 20:33:56 2014 +0100
    66.3 @@ -232,7 +232,7 @@
    66.4        | fm pos t = var(t,[]);
    66.5        (*entry point, and translation of a meta-formula*)
    66.6        fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
    66.7 -        | mt pos ((c as Const("==>", _)) $ p $ q) =
    66.8 +        | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) =
    66.9              Buildin("=>", [mt (not pos) p, mt pos q])
   66.10          | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   66.11  
    67.1 --- a/src/Provers/blast.ML	Fri Mar 21 15:12:03 2014 +0100
    67.2 +++ b/src/Provers/blast.ML	Fri Mar 21 20:33:56 2014 +0100
    67.3 @@ -419,11 +419,12 @@
    67.4  
    67.5  
    67.6  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    67.7 -fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
    67.8 +fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) =
    67.9 +      strip_Trueprop A :: strip_imp_prems B
   67.10    | strip_imp_prems _ = [];
   67.11  
   67.12  (* A1==>...An==>B  goes to B, where B is not an implication *)
   67.13 -fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
   67.14 +fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B
   67.15    | strip_imp_concl A = strip_Trueprop A;
   67.16  
   67.17  
   67.18 @@ -443,7 +444,7 @@
   67.19            else P :: delete_concl Ps
   67.20        | _ => P :: delete_concl Ps);
   67.21  
   67.22 -fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
   67.23 +fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) =
   67.24          skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
   67.25    | skoPrem _ _ P = P;
   67.26  
   67.27 @@ -1177,7 +1178,7 @@
   67.28  (*Make a list of all the parameters in a subgoal, even if nested*)
   67.29  local open Term
   67.30  in
   67.31 -fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
   67.32 +fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t
   67.33    | discard_foralls t = t;
   67.34  end;
   67.35  
    68.1 --- a/src/Provers/hypsubst.ML	Fri Mar 21 15:12:03 2014 +0100
    68.2 +++ b/src/Provers/hypsubst.ML	Fri Mar 21 20:33:56 2014 +0100
    68.3 @@ -104,8 +104,8 @@
    68.4  (*Locates a substitutable variable on the left (resp. right) of an equality
    68.5     assumption.  Returns the number of intervening assumptions. *)
    68.6  fun eq_var bnd novars =
    68.7 -  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    68.8 -        | eq_var_aux k (Const("==>",_) $ A $ B) =
    68.9 +  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
   68.10 +        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
   68.11                ((k, inspect_pair bnd novars
   68.12                      (Data.dest_eq (Data.dest_Trueprop A)))
   68.13                 handle TERM _ => eq_var_aux (k+1) B
    69.1 --- a/src/Provers/splitter.ML	Fri Mar 21 15:12:03 2014 +0100
    69.2 +++ b/src/Provers/splitter.ML	Fri Mar 21 20:33:56 2014 +0100
    69.3 @@ -57,7 +57,7 @@
    69.4  fun split_format_err () = error "Wrong format for split rule";
    69.5  
    69.6  fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
    69.7 -     Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
    69.8 +     Const(@{const_name Pure.eq}, _) $ (Var _ $ t) $ c => (case strip_comb t of
    69.9         (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
   69.10       | _ => split_format_err ())
   69.11     | _ => split_format_err ();
   69.12 @@ -393,9 +393,9 @@
   69.13        fun tac (t,i) =
   69.14            let val n = find_index (exists_Const (member (op =) cname_list o #1))
   69.15                                   (Logic.strip_assums_hyp t);
   69.16 -              fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _)
   69.17 +              fun first_prem_is_disj (Const (@{const_name Pure.imp}, _) $ (Const (c, _)
   69.18                      $ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or
   69.19 -              |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
   69.20 +              |   first_prem_is_disj (Const(@{const_name Pure.all},_)$Abs(_,_,t)) =
   69.21                                          first_prem_is_disj t
   69.22                |   first_prem_is_disj _ = false;
   69.23        (* does not work properly if the split variable is bound by a quantifier *)
    70.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 15:12:03 2014 +0100
    70.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 20:33:56 2014 +0100
    70.3 @@ -63,7 +63,7 @@
    70.4  
    70.5        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    70.6          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    70.7 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    70.8 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
    70.9               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
   70.10          let
   70.11            val _ $ A $ C = Envir.beta_norm X;
   70.12 @@ -78,7 +78,7 @@
   70.13        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   70.14          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   70.15            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   70.16 -            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
   70.17 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
   70.18                 (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
   70.19          let
   70.20            val _ $ A $ C = Envir.beta_norm Y;
   70.21 @@ -91,7 +91,7 @@
   70.22          end
   70.23  
   70.24        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   70.25 -        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   70.26 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
   70.27            (PAxm ("Pure.reflexive", _, _) % _) %%
   70.28              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
   70.29          let
   70.30 @@ -104,7 +104,7 @@
   70.31  
   70.32        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   70.33          (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
   70.34 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   70.35 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
   70.36              (PAxm ("Pure.reflexive", _, _) % _) %%
   70.37                (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
   70.38          let
   70.39 @@ -140,7 +140,7 @@
   70.40        | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   70.41          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   70.42            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   70.43 -            (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   70.44 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   70.45                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   70.46            SOME (equal_elim_axm %> C %> D %% prf2 %%
   70.47              (equal_elim_axm %> A %> C %% prf3 %%
   70.48 @@ -150,7 +150,7 @@
   70.49          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   70.50            (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   70.51              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   70.52 -              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   70.53 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   70.54                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   70.55            SOME (equal_elim_axm %> A %> B %% prf1 %%
   70.56              (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
   70.57 @@ -160,7 +160,7 @@
   70.58          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   70.59            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   70.60              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   70.61 -              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   70.62 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   70.63                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   70.64            SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
   70.65              (equal_elim_axm %> B %> D %% prf3 %%
   70.66 @@ -171,14 +171,14 @@
   70.67            (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   70.68              (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   70.69                (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   70.70 -                (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   70.71 +                (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   70.72                    (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   70.73            SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
   70.74              (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
   70.75                (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   70.76  
   70.77        | rew' ((prf as PAxm ("Pure.combination", _, _) %
   70.78 -        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   70.79 +        SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
   70.80            (PAxm ("Pure.reflexive", _, _) % _)) =
   70.81          let val (U, V) = (case T of
   70.82            Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   70.83 @@ -307,9 +307,9 @@
   70.84      val Hs' = Logic.strip_assums_hyp Q;
   70.85      val k = length Hs;
   70.86      val l = length params;
   70.87 -    fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
   70.88 +    fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
   70.89            mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
   70.90 -      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
   70.91 +      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
   70.92            mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
   70.93        | mk_prf _ _ _ _ _ prf = prf
   70.94    in
   70.95 @@ -324,9 +324,9 @@
   70.96      val Hs' = Logic.strip_assums_hyp Q;
   70.97      val k = length Hs;
   70.98      val l = length params;
   70.99 -    fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
  70.100 +    fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
  70.101            Abst (s, SOME T, mk_prf P prf)
  70.102 -      | mk_prf (Const ("==>", _) $ P $ Q) prf =
  70.103 +      | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
  70.104            AbsP ("H", SOME P, mk_prf Q prf)
  70.105        | mk_prf _ prf = prf
  70.106    in
    71.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Mar 21 15:12:03 2014 +0100
    71.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Mar 21 20:33:56 2014 +0100
    71.3 @@ -155,7 +155,7 @@
    71.4                | SOME T => (T, env));
    71.5              val (t, prf, cnstrts, env'', vTs') =
    71.6                mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
    71.7 -          in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
    71.8 +          in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
    71.9              cnstrts, env'', vTs')
   71.10            end
   71.11        | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
   71.12 @@ -173,7 +173,7 @@
   71.13        | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) =
   71.14            let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2
   71.15            in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of
   71.16 -              (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
   71.17 +              (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
   71.18                  add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts)
   71.19                    env'' vTs'' (u, u')
   71.20              | (t, prf1, cnstrts', env'', vTs'') =>
   71.21 @@ -185,7 +185,7 @@
   71.22        | mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
   71.23            let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
   71.24            in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
   71.25 -             (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   71.26 +             (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   71.27                   prf, cnstrts, env2, vTs2) =>
   71.28                 let val env3 = unifyT thy env2 T U
   71.29                 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
   71.30 @@ -194,12 +194,12 @@
   71.31                 let val (v, env3) = mk_var env2 Ts (U --> propT);
   71.32                 in
   71.33                   add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2
   71.34 -                   (u, Const ("all", (U --> propT) --> propT) $ v)
   71.35 +                   (u, Const ("Pure.all", (U --> propT) --> propT) $ v)
   71.36                 end)
   71.37            end
   71.38        | mk_cnstrts env Ts Hs vTs (cprf % NONE) =
   71.39            (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of
   71.40 -             (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   71.41 +             (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   71.42                   prf, cnstrts, env', vTs') =>
   71.43                 let val (t, env'') = mk_var env' Ts T
   71.44                 in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs')
   71.45 @@ -211,7 +211,7 @@
   71.46                   val (t, env3) = mk_var env2 Ts T
   71.47                 in
   71.48                   add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
   71.49 -                   (u, Const ("all", (T --> propT) --> propT) $ v)
   71.50 +                   (u, Const ("Pure.all", (T --> propT) --> propT) $ v)
   71.51                 end)
   71.52        | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
   71.53            mk_cnstrts_atom env vTs prop opTs prf
   71.54 @@ -309,10 +309,10 @@
   71.55    | prop_of0 Hs (AbsP (s, SOME t, prf)) =
   71.56        Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
   71.57    | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
   71.58 -      Const ("all", _) $ f => f $ t
   71.59 +      Const ("Pure.all", _) $ f => f $ t
   71.60      | _ => error "prop_of: all expected")
   71.61    | prop_of0 Hs (prf1 %% prf2) = (case head_norm (prop_of0 Hs prf1) of
   71.62 -      Const ("==>", _) $ P $ Q => Q
   71.63 +      Const ("Pure.imp", _) $ P $ Q => Q
   71.64      | _ => error "prop_of: ==> expected")
   71.65    | prop_of0 Hs (Hyp t) = t
   71.66    | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
    72.1 --- a/src/Pure/Syntax/simple_syntax.ML	Fri Mar 21 15:12:03 2014 +0100
    72.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Fri Mar 21 20:33:56 2014 +0100
    72.3 @@ -107,12 +107,12 @@
    72.4   (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
    72.5    term2 env T) x
    72.6  and term2 env T x =
    72.7 - (equal env "==" ||
    72.8 + (equal env ||
    72.9    term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   72.10    term3 env T) x
   72.11 -and equal env eq x =
   72.12 - (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
   72.13 -   Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   72.14 +and equal env x =
   72.15 + (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) =>
   72.16 +   Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   72.17  and term3 env T x =
   72.18   (idt >> Free ||
   72.19    var -- constraint >> Var ||
    73.1 --- a/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 15:12:03 2014 +0100
    73.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 20:33:56 2014 +0100
    73.3 @@ -174,7 +174,7 @@
    73.4          (case Ast.unfold_ast_p "_asms" asms of
    73.5            (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
    73.6          | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
    73.7 -      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
    73.8 +      in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
    73.9    | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
   73.10  
   73.11  
   73.12 @@ -382,7 +382,8 @@
   73.13  fun impl_ast_tr' asts =
   73.14    if no_brackets () then raise Match
   73.15    else
   73.16 -    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
   73.17 +    (case Ast.unfold_ast_p "\\<^const>Pure.imp"
   73.18 +        (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
   73.19        (prems as _ :: _ :: _, concl) =>
   73.20          let
   73.21            val (asms, asm) = split_last prems;
   73.22 @@ -498,7 +499,7 @@
   73.23    ("_abs", fn _ => abs_ast_tr'),
   73.24    ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   73.25    ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   73.26 -  ("\\<^const>==>", fn _ => impl_ast_tr'),
   73.27 +  ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
   73.28    ("_index", fn _ => index_ast_tr')];
   73.29  
   73.30  end;
    74.1 --- a/src/Pure/conv.ML	Fri Mar 21 15:12:03 2014 +0100
    74.2 +++ b/src/Pure/conv.ML	Fri Mar 21 20:33:56 2014 +0100
    74.3 @@ -140,17 +140,17 @@
    74.4  
    74.5  fun forall_conv cv ctxt ct =
    74.6    (case Thm.term_of ct of
    74.7 -    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
    74.8 +    Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
    74.9    | _ => raise CTERM ("forall_conv", [ct]));
   74.10  
   74.11  fun implies_conv cv1 cv2 ct =
   74.12    (case Thm.term_of ct of
   74.13 -    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   74.14 +    Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   74.15    | _ => raise CTERM ("implies_conv", [ct]));
   74.16  
   74.17  fun implies_concl_conv cv ct =
   74.18    (case Thm.term_of ct of
   74.19 -    Const ("==>", _) $ _ $ _ => arg_conv cv ct
   74.20 +    Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
   74.21    | _ => raise CTERM ("implies_concl_conv", [ct]));
   74.22  
   74.23  
    75.1 --- a/src/Pure/drule.ML	Fri Mar 21 15:12:03 2014 +0100
    75.2 +++ b/src/Pure/drule.ML	Fri Mar 21 20:33:56 2014 +0100
    75.3 @@ -126,7 +126,7 @@
    75.4  (* A1==>...An==>B  goes to B, where B is not an implication *)
    75.5  fun strip_imp_concl ct =
    75.6    (case Thm.term_of ct of
    75.7 -    Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
    75.8 +    Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
    75.9    | _ => ct);
   75.10  
   75.11  (*The premises of a theorem, as a cterm list*)
   75.12 @@ -706,7 +706,7 @@
   75.13  val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
   75.14  
   75.15  fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
   75.16 -  | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
   75.17 +  | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
   75.18    | is_norm_hhf (Abs _ $ _) = false
   75.19    | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u
   75.20    | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
    76.1 --- a/src/Pure/goal.ML	Fri Mar 21 15:12:03 2014 +0100
    76.2 +++ b/src/Pure/goal.ML	Fri Mar 21 20:33:56 2014 +0100
    76.3 @@ -327,8 +327,8 @@
    76.4  
    76.5  (* non-atomic goal assumptions *)
    76.6  
    76.7 -fun non_atomic (Const ("==>", _) $ _ $ _) = true
    76.8 -  | non_atomic (Const ("all", _) $ _) = true
    76.9 +fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true
   76.10 +  | non_atomic (Const ("Pure.all", _) $ _) = true
   76.11    | non_atomic _ = false;
   76.12  
   76.13  fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
    77.1 --- a/src/Pure/logic.ML	Fri Mar 21 15:12:03 2014 +0100
    77.2 +++ b/src/Pure/logic.ML	Fri Mar 21 20:33:56 2014 +0100
    77.3 @@ -93,14 +93,14 @@
    77.4  
    77.5  (** all **)
    77.6  
    77.7 -fun all_const T = Const ("all", (T --> propT) --> propT);
    77.8 +fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
    77.9  
   77.10  fun all v t = all_const (Term.fastype_of v) $ lambda v t;
   77.11  
   77.12 -fun is_all (Const ("all", _) $ Abs _) = true
   77.13 +fun is_all (Const ("Pure.all", _) $ Abs _) = true
   77.14    | is_all _ = false;
   77.15  
   77.16 -fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
   77.17 +fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
   77.18        let val (x, b) = Term.dest_abs abs  (*potentially slow*)
   77.19        in ((x, T), b) end
   77.20    | dest_all t = raise TERM ("dest_all", [t]);
   77.21 @@ -113,19 +113,19 @@
   77.22  
   77.23  fun mk_equals (t, u) =
   77.24    let val T = Term.fastype_of t
   77.25 -  in Const ("==", T --> T --> propT) $ t $ u end;
   77.26 +  in Const ("Pure.eq", T --> T --> propT) $ t $ u end;
   77.27  
   77.28 -fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   77.29 +fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
   77.30    | dest_equals t = raise TERM ("dest_equals", [t]);
   77.31  
   77.32  
   77.33  (** implies **)
   77.34  
   77.35 -val implies = Const ("==>", propT --> propT --> propT);
   77.36 +val implies = Const ("Pure.imp", propT --> propT --> propT);
   77.37  
   77.38  fun mk_implies (A, B) = implies $ A $ B;
   77.39  
   77.40 -fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   77.41 +fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B)
   77.42    | dest_implies A = raise TERM ("dest_implies", [A]);
   77.43  
   77.44  
   77.45 @@ -136,28 +136,28 @@
   77.46    | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   77.47  
   77.48  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   77.49 -fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   77.50 +fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
   77.51    | strip_imp_prems _ = [];
   77.52  
   77.53  (* A1==>...An==>B  goes to B, where B is not an implication *)
   77.54 -fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   77.55 +fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
   77.56    | strip_imp_concl A = A : term;
   77.57  
   77.58  (*Strip and return premises: (i, [], A1==>...Ai==>B)
   77.59      goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   77.60    if  i<0 or else i too big then raises  TERM*)
   77.61  fun strip_prems (0, As, B) = (As, B)
   77.62 -  | strip_prems (i, As, Const("==>", _) $ A $ B) =
   77.63 +  | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) =
   77.64          strip_prems (i-1, A::As, B)
   77.65    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   77.66  
   77.67  (*Count premises -- quicker than (length o strip_prems) *)
   77.68 -fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
   77.69 +fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
   77.70    | count_prems _ = 0;
   77.71  
   77.72  (*Select Ai from A1 ==>...Ai==>B*)
   77.73 -fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   77.74 -  | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   77.75 +fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
   77.76 +  | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
   77.77    | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   77.78  
   77.79  (*strip a proof state (Horn clause):
   77.80 @@ -395,46 +395,46 @@
   77.81  
   77.82  fun lift_abs inc =
   77.83    let
   77.84 -    fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   77.85 -      | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   77.86 +    fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
   77.87 +      | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   77.88        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   77.89    in lift [] end;
   77.90  
   77.91  fun lift_all inc =
   77.92    let
   77.93 -    fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   77.94 -      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   77.95 +    fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
   77.96 +      | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   77.97        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   77.98    in lift [] end;
   77.99  
  77.100  (*Strips assumptions in goal, yielding list of hypotheses.   *)
  77.101  fun strip_assums_hyp B =
  77.102    let
  77.103 -    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
  77.104 -      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
  77.105 +    fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B
  77.106 +      | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) =
  77.107            strip (map (incr_boundvars 1) Hs) t
  77.108        | strip Hs B = rev Hs
  77.109    in strip [] B end;
  77.110  
  77.111  (*Strips assumptions in goal, yielding conclusion.   *)
  77.112 -fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
  77.113 -  | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
  77.114 +fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
  77.115 +  | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t
  77.116    | strip_assums_concl B = B;
  77.117  
  77.118  (*Make a list of all the parameters in a subgoal, even if nested*)
  77.119 -fun strip_params (Const("==>", _) $ H $ B) = strip_params B
  77.120 -  | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
  77.121 +fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
  77.122 +  | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
  77.123    | strip_params B = [];
  77.124  
  77.125  (*test for nested meta connectives in prems*)
  77.126  val has_meta_prems =
  77.127    let
  77.128 -    fun is_meta (Const ("==", _) $ _ $ _) = true
  77.129 -      | is_meta (Const ("==>", _) $ _ $ _) = true
  77.130 -      | is_meta (Const ("all", _) $ _) = true
  77.131 +    fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true
  77.132 +      | is_meta (Const ("Pure.imp", _) $ _ $ _) = true
  77.133 +      | is_meta (Const ("Pure.all", _) $ _) = true
  77.134        | is_meta _ = false;
  77.135 -    fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
  77.136 -      | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
  77.137 +    fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B
  77.138 +      | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B
  77.139        | ex_meta _ = false;
  77.140    in ex_meta end;
  77.141  
  77.142 @@ -444,10 +444,10 @@
  77.143  fun remove_params j n A =
  77.144      if j=0 andalso n<=0 then A  (*nothing left to do...*)
  77.145      else case A of
  77.146 -        Const("==>", _) $ H $ B =>
  77.147 +        Const("Pure.imp", _) $ H $ B =>
  77.148            if n=1 then                           (remove_params j (n-1) B)
  77.149            else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
  77.150 -      | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
  77.151 +      | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t
  77.152        | _ => if n>0 then raise TERM("remove_params", [A])
  77.153               else A;
  77.154  
  77.155 @@ -460,9 +460,9 @@
  77.156      in list_all (vars, remove_params (length vars) n A) end;
  77.157  
  77.158  (*Makes parameters in a goal have the names supplied by the list cs.*)
  77.159 -fun list_rename_params cs (Const ("==>", _) $ A $ B) =
  77.160 +fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) =
  77.161        implies $ A $ list_rename_params cs B
  77.162 -  | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
  77.163 +  | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) =
  77.164        a $ Abs (c, T, list_rename_params cs t)
  77.165    | list_rename_params cs B = B;
  77.166  
  77.167 @@ -480,12 +480,12 @@
  77.168        Unless nasms<0, it can terminate the recursion early; that allows
  77.169    erule to work on assumptions of the form P==>Q.*)
  77.170  fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
  77.171 -  | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
  77.172 +  | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
  77.173        strip_assums_imp (nasms-1, H::Hs, B)
  77.174    | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
  77.175  
  77.176  (*Strips OUTER parameters only.*)
  77.177 -fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
  77.178 +fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) =
  77.179        strip_assums_all ((a,T)::params, t)
  77.180    | strip_assums_all (params, B) = (params, B);
  77.181  
    78.1 --- a/src/Pure/more_thm.ML	Fri Mar 21 15:12:03 2014 +0100
    78.2 +++ b/src/Pure/more_thm.ML	Fri Mar 21 20:33:56 2014 +0100
    78.3 @@ -127,7 +127,7 @@
    78.4    let
    78.5      val cert = Thm.cterm_of (Thm.theory_of_cterm t);
    78.6      val T = #T (Thm.rep_cterm t);
    78.7 -  in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
    78.8 +  in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
    78.9  
   78.10  fun all t A = all_name ("", t) A;
   78.11  
   78.12 @@ -136,22 +136,22 @@
   78.13  
   78.14  fun dest_implies ct =
   78.15    (case Thm.term_of ct of
   78.16 -    Const ("==>", _) $ _ $ _ => dest_binop ct
   78.17 +    Const ("Pure.imp", _) $ _ $ _ => dest_binop ct
   78.18    | _ => raise TERM ("dest_implies", [Thm.term_of ct]));
   78.19  
   78.20  fun dest_equals ct =
   78.21    (case Thm.term_of ct of
   78.22 -    Const ("==", _) $ _ $ _ => dest_binop ct
   78.23 +    Const ("Pure.eq", _) $ _ $ _ => dest_binop ct
   78.24    | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
   78.25  
   78.26  fun dest_equals_lhs ct =
   78.27    (case Thm.term_of ct of
   78.28 -    Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
   78.29 +    Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct
   78.30    | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
   78.31  
   78.32  fun dest_equals_rhs ct =
   78.33    (case Thm.term_of ct of
   78.34 -    Const ("==", _) $ _ $ _ => Thm.dest_arg ct
   78.35 +    Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct
   78.36    | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
   78.37  
   78.38  val lhs_of = dest_equals_lhs o Thm.cprop_of;
   78.39 @@ -337,7 +337,7 @@
   78.40  
   78.41  fun forall_elim_var i th =
   78.42    forall_elim_vars_aux
   78.43 -    (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
   78.44 +    (fn Const ("Pure.all", _) $ Abs (a, T, _) => [(a, T)]
   78.45        | _ => raise THM ("forall_elim_vars", i, [th])) i th;
   78.46  
   78.47  end;
    79.1 --- a/src/Pure/proofterm.ML	Fri Mar 21 15:12:03 2014 +0100
    79.2 +++ b/src/Pure/proofterm.ML	Fri Mar 21 20:33:56 2014 +0100
    79.3 @@ -865,9 +865,9 @@
    79.4      fun mk_app b (i, j, prf) =
    79.5            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
    79.6  
    79.7 -    fun lift Us bs i j (Const ("==>", _) $ A $ B) =
    79.8 +    fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
    79.9              AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
   79.10 -      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
   79.11 +      | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
   79.12              Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
   79.13        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
   79.14              map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
   79.15 @@ -886,9 +886,9 @@
   79.16  fun mk_asm_prf t i m =
   79.17    let
   79.18      fun imp_prf _ i 0 = PBound i
   79.19 -      | imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
   79.20 +      | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
   79.21        | imp_prf _ i _ = PBound i;
   79.22 -    fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
   79.23 +    fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
   79.24        | all_prf t = imp_prf t (~i) m
   79.25    in all_prf t end;
   79.26  
   79.27 @@ -899,9 +899,9 @@
   79.28  
   79.29  (***** Composition of object rule with proof state *****)
   79.30  
   79.31 -fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) =
   79.32 +fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
   79.33        AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
   79.34 -  | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) =
   79.35 +  | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) =
   79.36        Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
   79.37    | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
   79.38        map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
   79.39 @@ -1091,9 +1091,9 @@
   79.40        if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   79.41    else vs;
   79.42  
   79.43 -fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
   79.44 +fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) =
   79.45        add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
   79.46 -  | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) =
   79.47 +  | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) =
   79.48        add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
   79.49    | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
   79.50    | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
   79.51 @@ -1105,8 +1105,8 @@
   79.52    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   79.53    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
   79.54  
   79.55 -fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
   79.56 -  | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   79.57 +fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
   79.58 +  | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
   79.59    | prop_vars t = (case strip_comb t of
   79.60        (Var (ixn, _), _) => [ixn] | _ => []);
   79.61  
   79.62 @@ -1196,7 +1196,7 @@
   79.63                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
   79.64                  | (_, x) => (false, x)) insts
   79.65            in ([], false, insts' @ map (pair false) ts'', prf) end
   79.66 -    and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
   79.67 +    and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) =
   79.68            union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
   79.69        | needed (Var (ixn, _)) (_::_) _ = [ixn]
   79.70        | needed _ _ _ = [];
    80.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 15:12:03 2014 +0100
    80.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 20:33:56 2014 +0100
    80.3 @@ -169,7 +169,7 @@
    80.4      ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
    80.5      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
    80.6      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
    80.7 -    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
    80.8 +    (const "Pure.imp",  typ "prop => prop => prop",     Delimfix "op ==>"),
    80.9      (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
   80.10      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   80.11      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
   80.12 @@ -184,9 +184,9 @@
   80.13      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
   80.14      ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
   80.15      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
   80.16 -    (const "==",          typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
   80.17 -    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
   80.18 -    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
   80.19 +    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
   80.20 +    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
   80.21 +    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
   80.22      ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
   80.23      ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   80.24      ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
   80.25 @@ -195,15 +195,15 @@
   80.26    #> Sign.add_syntax ("HTML", false)
   80.27     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   80.28    #> Sign.add_consts
   80.29 -   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
   80.30 -    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   80.31 -    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
   80.32 +   [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
   80.33 +    (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   80.34 +    (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
   80.35      (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
   80.36      (qualify (Binding.name "type"), typ "'a itself", NoSyn),
   80.37      (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
   80.38 -  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
   80.39 -  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
   80.40 -  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
   80.41 +  #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
   80.42 +  #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
   80.43 +  #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
   80.44    #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
   80.45    #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
   80.46    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
    81.1 --- a/src/Pure/raw_simplifier.ML	Fri Mar 21 15:12:03 2014 +0100
    81.2 +++ b/src/Pure/raw_simplifier.ML	Fri Mar 21 20:33:56 2014 +0100
    81.3 @@ -599,7 +599,7 @@
    81.4    | is_full_cong_prems [] _ = false
    81.5    | is_full_cong_prems (p :: prems) varpairs =
    81.6        (case Logic.strip_assums_concl p of
    81.7 -        Const ("==", _) $ lhs $ rhs =>
    81.8 +        Const ("Pure.eq", _) $ lhs $ rhs =>
    81.9            let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
   81.10              is_Var x andalso forall is_Bound xs andalso
   81.11              not (has_duplicates (op =) xs) andalso xs = ys andalso
   81.12 @@ -981,7 +981,7 @@
   81.13        let
   81.14          fun is_simple ({thm, ...}: rrule) =
   81.15            (case Thm.prop_of thm of
   81.16 -            Const ("==", _) $ _ $ _ => true
   81.17 +            Const ("Pure.eq", _) $ _ $ _ => true
   81.18            | _ => false);
   81.19          fun sort [] (re1, re2) = re1 @ re2
   81.20            | sort (rr :: rrs) (re1, re2) =
   81.21 @@ -1099,7 +1099,7 @@
   81.22                  end
   81.23              | t $ _ =>
   81.24                (case t of
   81.25 -                Const ("==>", _) $ _  => impc t0 ctxt
   81.26 +                Const ("Pure.imp", _) $ _  => impc t0 ctxt
   81.27                | Abs _ =>
   81.28                    let val thm = Thm.beta_conversion false t0
   81.29                    in
    82.1 --- a/src/Pure/term.ML	Fri Mar 21 15:12:03 2014 +0100
    82.2 +++ b/src/Pure/term.ML	Fri Mar 21 20:33:56 2014 +0100
    82.3 @@ -579,11 +579,11 @@
    82.4  val propT : typ = Type ("prop",[]);
    82.5  
    82.6  (* maps  !!x1...xn. t   to   t  *)
    82.7 -fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
    82.8 +fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t))  =  strip_all_body t
    82.9    | strip_all_body t  =  t;
   82.10  
   82.11  (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   82.12 -fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   82.13 +fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t))  =
   82.14                  (a,T) :: strip_all_vars t
   82.15    | strip_all_vars t  =  [] : (string*typ) list;
   82.16  
    83.1 --- a/src/Pure/thm.ML	Fri Mar 21 15:12:03 2014 +0100
    83.2 +++ b/src/Pure/thm.ML	Fri Mar 21 20:33:56 2014 +0100
    83.3 @@ -687,7 +687,7 @@
    83.4      fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
    83.5    in
    83.6      case prop of
    83.7 -      Const ("==>", _) $ A $ B =>
    83.8 +      Const ("Pure.imp", _) $ A $ B =>
    83.9          if A aconv propA then
   83.10            Thm (deriv_rule2 (curry Proofterm.%%) der derA,
   83.11             {thy = merge_thys2 thAB thA,
   83.12 @@ -741,7 +741,7 @@
   83.13      (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
   83.14      (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
   83.15    (case prop of
   83.16 -    Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
   83.17 +    Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
   83.18        if T <> qary then
   83.19          raise THM ("forall_elim: type mismatch", 0, [th])
   83.20        else
   83.21 @@ -778,7 +778,7 @@
   83.22  *)
   83.23  fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
   83.24    (case prop of
   83.25 -    (eq as Const ("==", _)) $ t $ u =>
   83.26 +    (eq as Const ("Pure.eq", _)) $ t $ u =>
   83.27        Thm (deriv_rule1 Proofterm.symmetric der,
   83.28         {thy = thy,
   83.29          tags = [],
   83.30 @@ -803,7 +803,7 @@
   83.31      fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   83.32    in
   83.33      case (prop1, prop2) of
   83.34 -      ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
   83.35 +      ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
   83.36          if not (u aconv u') then err "middle term"
   83.37          else
   83.38            Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
   83.39 @@ -911,8 +911,8 @@
   83.40        | _ => raise THM ("combination: not function type", 0, [th1, th2]));
   83.41    in
   83.42      (case (prop1, prop2) of
   83.43 -      (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   83.44 -       Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   83.45 +      (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
   83.46 +       Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
   83.47          (chktypes fT tT;
   83.48            Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
   83.49             {thy = merge_thys2 th1 th2,
   83.50 @@ -939,7 +939,7 @@
   83.51      fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   83.52    in
   83.53      (case (prop1, prop2) of
   83.54 -      (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
   83.55 +      (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
   83.56          if A aconv A' andalso B aconv B' then
   83.57            Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
   83.58             {thy = merge_thys2 th1 th2,
   83.59 @@ -967,7 +967,7 @@
   83.60      fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
   83.61    in
   83.62      (case prop1 of
   83.63 -      Const ("==", _) $ A $ B =>
   83.64 +      Const ("Pure.eq", _) $ A $ B =>
   83.65          if prop2 aconv A then
   83.66            Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
   83.67             {thy = merge_thys2 th1 th2,
   83.68 @@ -1472,17 +1472,17 @@
   83.69  (* strip_apply f B A strips off all assumptions/parameters from A
   83.70     introduced by lifting over B, and applies f to remaining part of A*)
   83.71  fun strip_apply f =
   83.72 -  let fun strip (Const ("==>", _) $ _  $ B1)
   83.73 -                (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
   83.74 -        | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
   83.75 -                (      Const ("all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
   83.76 +  let fun strip (Const ("Pure.imp", _) $ _  $ B1)
   83.77 +                (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
   83.78 +        | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
   83.79 +                (      Const ("Pure.all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
   83.80          | strip _ A = f A
   83.81    in strip end;
   83.82  
   83.83 -fun strip_lifted (Const ("==>", _) $ _ $ B1)
   83.84 -                 (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
   83.85 -  | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
   83.86 -                 (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
   83.87 +fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1)
   83.88 +                 (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2
   83.89 +  | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1))
   83.90 +                 (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
   83.91    | strip_lifted _ A = A;
   83.92  
   83.93  (*Use the alist to rename all bound variables and some unknowns in a term
   83.94 @@ -1532,10 +1532,10 @@
   83.95  
   83.96  (*strip off pairs of assumptions/parameters in parallel -- they are
   83.97    identical because of lifting*)
   83.98 -fun strip_assums2 (Const("==>", _) $ _ $ B1,
   83.99 -                   Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
  83.100 -  | strip_assums2 (Const("all",_)$Abs(a,T,t1),
  83.101 -                   Const("all",_)$Abs(_,_,t2)) =
  83.102 +fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1,
  83.103 +                   Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2)
  83.104 +  | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1),
  83.105 +                   Const("Pure.all",_)$Abs(_,_,t2)) =
  83.106        let val (B1,B2) = strip_assums2 (t1,t2)
  83.107        in  (Abs(a,T,B1), Abs(a,T,B2))  end
  83.108    | strip_assums2 BB = BB;
  83.109 @@ -1543,13 +1543,13 @@
  83.110  
  83.111  (*Faster normalization: skip assumptions that were lifted over*)
  83.112  fun norm_term_skip env 0 t = Envir.norm_term env t
  83.113 -  | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
  83.114 +  | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) =
  83.115        let
  83.116          val T' = Envir.subst_type (Envir.type_env env) T
  83.117          (*Must instantiate types of parameters because they are flattened;
  83.118            this could be a NEW parameter*)
  83.119        in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
  83.120 -  | norm_term_skip env n (Const ("==>", _) $ A $ B) =
  83.121 +  | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) =
  83.122        Logic.mk_implies (A, norm_term_skip env (n - 1) B)
  83.123    | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
  83.124  
    84.1 --- a/src/Sequents/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
    84.2 +++ b/src/Sequents/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
    84.3 @@ -29,7 +29,7 @@
    84.4  
    84.5  (*Make meta-equalities.*)
    84.6  fun mk_meta_eq ctxt th = case concl_of th of
    84.7 -    Const("==",_)$_$_           => th
    84.8 +    Const(@{const_name Pure.eq},_)$_$_ => th
    84.9    | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
   84.10          (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
   84.11               ([], [p]) =>
    85.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 21 15:12:03 2014 +0100
    85.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 21 20:33:56 2014 +0100
    85.3 @@ -163,7 +163,7 @@
    85.4      val _ = if fastype_of t <> propT
    85.5        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    85.6        else ();
    85.7 -    val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
    85.8 +    val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    85.9      val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
   85.10       of SOME Holds => true
   85.11        | _ => false;
    86.1 --- a/src/Tools/Code/code_symbol.ML	Fri Mar 21 15:12:03 2014 +0100
    86.2 +++ b/src/Tools/Code/code_symbol.ML	Fri Mar 21 20:33:56 2014 +0100
    86.3 @@ -88,8 +88,8 @@
    86.4  in
    86.5  
    86.6  fun default_base (Constant "") = "value"
    86.7 -  | default_base (Constant "==>") = "follows"
    86.8 -  | default_base (Constant "==") = "meta_eq"
    86.9 +  | default_base (Constant @{const_name Pure.imp}) = "follows"
   86.10 +  | default_base (Constant @{const_name Pure.eq}) = "meta_eq"
   86.11    | default_base (Constant c) = base c
   86.12    | default_base (Type_Constructor tyco) = base tyco
   86.13    | default_base (Type_Class class) = base class
    87.1 --- a/src/Tools/induct.ML	Fri Mar 21 15:12:03 2014 +0100
    87.2 +++ b/src/Tools/induct.ML	Fri Mar 21 20:33:56 2014 +0100
    87.3 @@ -162,7 +162,7 @@
    87.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
    87.5  
    87.6  val rearrange_eqs_simproc =
    87.7 -  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
    87.8 +  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
    87.9      (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
   87.10  
   87.11  
   87.12 @@ -644,14 +644,16 @@
   87.13  
   87.14  local
   87.15  
   87.16 -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
   87.17 +fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) =
   87.18 +      c $ Abs (a, T, goal_prefix k B)
   87.19    | goal_prefix 0 _ = Term.dummy_prop
   87.20 -  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
   87.21 +  | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) =
   87.22 +      c $ A $ goal_prefix (k - 1) B
   87.23    | goal_prefix _ _ = Term.dummy_prop;
   87.24  
   87.25 -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
   87.26 +fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1
   87.27    | goal_params 0 _ = 0
   87.28 -  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
   87.29 +  | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B
   87.30    | goal_params _ _ = 0;
   87.31  
   87.32  fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   87.33 @@ -670,11 +672,13 @@
   87.34            [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
   87.35             (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
   87.36  
   87.37 -    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
   87.38 +    fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
   87.39 +          goal_concl k ((a, T) :: xs) B
   87.40        | goal_concl 0 xs B =
   87.41            if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
   87.42            else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
   87.43 -      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
   87.44 +      | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) =
   87.45 +          goal_concl (k - 1) xs B
   87.46        | goal_concl _ _ _ = NONE;
   87.47    in
   87.48      (case goal_concl n [] goal of
    88.1 --- a/src/Tools/misc_legacy.ML	Fri Mar 21 15:12:03 2014 +0100
    88.2 +++ b/src/Tools/misc_legacy.ML	Fri Mar 21 20:33:56 2014 +0100
    88.3 @@ -130,9 +130,9 @@
    88.4      H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    88.5    Main difference from strip_assums concerns parameters:
    88.6      it replaces the bound variables by free variables.  *)
    88.7 -fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    88.8 +fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) =
    88.9        strip_context_aux (params, H :: Hs, B)
   88.10 -  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
   88.11 +  | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) =
   88.12        let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
   88.13        in strip_context_aux ((b, T) :: params, Hs, u) end
   88.14    | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    89.1 --- a/src/Tools/nbe.ML	Fri Mar 21 15:12:03 2014 +0100
    89.2 +++ b/src/Tools/nbe.ML	Fri Mar 21 20:33:56 2014 +0100
    89.3 @@ -586,7 +586,7 @@
    89.4    let
    89.5      val thy = Proof_Context.theory_of ctxt;
    89.6      val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
    89.7 -    val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
    89.8 +    val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
    89.9      val rhs = Thm.cterm_of thy raw_rhs;
   89.10    in Thm.mk_binop eq lhs rhs end;
   89.11  
    90.1 --- a/src/Tools/quickcheck.ML	Fri Mar 21 15:12:03 2014 +0100
    90.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 21 20:33:56 2014 +0100
    90.3 @@ -358,7 +358,7 @@
    90.4      val lthy = Proof.context_of state;
    90.5      val thy = Proof.theory_of state;
    90.6      val _ = message lthy "Quickchecking..."
    90.7 -    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
    90.8 +    fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
    90.9        | strip t = t;
   90.10      val {goal = st, ...} = Proof.raw_goal state;
   90.11      val (gi, frees) = Logic.goal_params (prop_of st) i;