merged
authorwenzelm
Fri Mar 21 20:39:54 2014 +0100 (2014-03-21)
changeset 562462b2bcf4ecb48
parent 56238 5d147e1e18d1
parent 56245 84fc7dfa3cd4
child 56247 1ad01f98dc3e
merged
     1.1 --- a/NEWS	Fri Mar 21 15:36:00 2014 +0000
     1.2 +++ b/NEWS	Fri Mar 21 20:39:54 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:36:00 2014 +0000
     2.2 +++ b/src/CCL/Wfd.thy	Fri Mar 21 20:39:54 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/Codegen/Setup.thy	Fri Mar 21 15:36:00 2014 +0000
     3.2 +++ b/src/Doc/Codegen/Setup.thy	Fri Mar 21 20:39:54 2014 +0100
     3.3 @@ -19,10 +19,10 @@
     3.4  let
     3.5    val typ = Simple_Syntax.read_typ;
     3.6  in
     3.7 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
     3.8 +  Sign.del_syntax (Symbol.xsymbolsN, false)
     3.9     [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    3.10      ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    3.11 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    3.12 +  Sign.add_syntax (Symbol.xsymbolsN, false)
    3.13     [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    3.14      ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    3.15  end
     4.1 --- a/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 15:36:00 2014 +0000
     4.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 20:39:54 2014 +0100
     4.3 @@ -850,7 +850,7 @@
     4.4    @{text "#A \<equiv> A"} \\[1ex]
     4.5    @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
     4.6    @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
     4.7 -  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
     4.8 +  @{text "type :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
     4.9    @{text "(unspecified)"} \\
    4.10    \end{tabular}
    4.11    \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
     5.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Fri Mar 21 15:36:00 2014 +0000
     5.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Fri Mar 21 20:39:54 2014 +0100
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5  (* THEOREMS *)
     5.6  notation (Rule output)
     5.7 -  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
     5.8 +  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
     5.9  
    5.10  syntax (Rule output)
    5.11    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    5.12 @@ -28,7 +28,7 @@
    5.13    "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    5.14  
    5.15  notation (IfThen output)
    5.16 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    5.17 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    5.18  syntax (IfThen output)
    5.19    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    5.20    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    5.21 @@ -36,7 +36,7 @@
    5.22    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    5.23  
    5.24  notation (IfThenNoBox output)
    5.25 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    5.26 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    5.27  syntax (IfThenNoBox output)
    5.28    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    5.29    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
     6.1 --- a/src/FOL/simpdata.ML	Fri Mar 21 15:36:00 2014 +0000
     6.2 +++ b/src/FOL/simpdata.ML	Fri Mar 21 20:39:54 2014 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4    error("conclusion must be a =-equality or <->");;
     6.5  
     6.6  fun mk_eq th = case concl_of th of
     6.7 -    Const("==",_)$_$_           => th
     6.8 +    Const(@{const_name Pure.eq},_)$_$_ => th
     6.9    | _ $ (Const(@{const_name eq},_)$_$_)   => mk_meta_eq th
    6.10    | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
    6.11    | _ $ (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
     7.1 --- a/src/FOLP/hypsubst.ML	Fri Mar 21 15:36:00 2014 +0000
     7.2 +++ b/src/FOLP/hypsubst.ML	Fri Mar 21 20:39:54 2014 +0100
     7.3 @@ -58,8 +58,8 @@
     7.4     assumption.  Returns the number of intervening assumptions, paried with
     7.5     the rule asm_rl (resp. sym). *)
     7.6  fun eq_var bnd =
     7.7 -  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
     7.8 -        | eq_var_aux k (Const("==>",_) $ A $ B) =
     7.9 +  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
    7.10 +        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
    7.11                ((k, inspect_pair bnd (dest_eq A))
    7.12                        (*Exception Match comes from inspect_pair or dest_eq*)
    7.13                 handle Match => eq_var_aux (k+1) B)
     8.1 --- a/src/FOLP/simp.ML	Fri Mar 21 15:36:00 2014 +0000
     8.2 +++ b/src/FOLP/simp.ML	Fri Mar 21 20:39:54 2014 +0100
     8.3 @@ -405,10 +405,10 @@
     8.4      else ();
     8.5  
     8.6  (* Skip the first n hyps of a goal, and return the rest in generalized form *)
     8.7 -fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
     8.8 +fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) =
     8.9          if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
    8.10          else strip_varify(B,n-1,vs)
    8.11 -  | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
    8.12 +  | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) =
    8.13          strip_varify(t,n,Var(("?",length vs),T)::vs)
    8.14    | strip_varify  _  = [];
    8.15  
     9.1 --- a/src/HOL/Code_Evaluation.thy	Fri Mar 21 15:36:00 2014 +0000
     9.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Mar 21 20:39:54 2014 +0100
     9.3 @@ -85,8 +85,9 @@
     9.4  begin
     9.5  
     9.6  definition
     9.7 -  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
     9.8 -     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
     9.9 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) =
    9.10 +    Const (STR ''Pure.dummy_pattern'')
    9.11 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    9.12  
    9.13  instance ..
    9.14  
    10.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 15:36:00 2014 +0000
    10.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 20:39:54 2014 +0100
    10.3 @@ -84,7 +84,7 @@
    10.4      (* The result of the quantifier elimination *)
    10.5      val (th, tac) =
    10.6        (case (prop_of pre_thm) of
    10.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    10.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    10.9            let
   10.10              val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
   10.11            in
    11.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 15:36:00 2014 +0000
    11.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 20:39:54 2014 +0100
    11.3 @@ -64,7 +64,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 = linr_oracle (ctxt, Envir.eta_long [] t1)
   11.10      in 
   11.11         ((pth RS iffD2) RS pre_thm,
    12.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Mar 21 15:36:00 2014 +0000
    12.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Mar 21 20:39:54 2014 +0100
    12.3 @@ -184,9 +184,9 @@
    12.4     | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
    12.5     | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    12.6     | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    12.7 -   | Const ("==>", _) $ _ $ _ => find_args bounds tm
    12.8 -   | Const ("==", _) $ _ $ _ => find_args bounds tm
    12.9 -   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   12.10 +   | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
   12.11 +   | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
   12.12 +   | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   12.13     | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
   12.14     | _ => Thm.dest_fun2 tm)
   12.15    and find_args bounds tm =
    13.1 --- a/src/HOL/Decision_Procs/langford.ML	Fri Mar 21 15:36:00 2014 +0000
    13.2 +++ b/src/HOL/Decision_Procs/langford.ML	Fri Mar 21 20:39:54 2014 +0100
    13.3 @@ -204,13 +204,13 @@
    13.4            else Thm.dest_fun2 tm
    13.5        | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    13.6        | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    13.7 -      | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    13.8 +      | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    13.9        | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   13.10        | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
   13.11        | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   13.12        | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   13.13 -      | Const ("==>", _) $ _ $ _ => find_args bounds tm
   13.14 -      | Const ("==", _) $ _ $ _ => find_args bounds tm
   13.15 +      | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
   13.16 +      | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
   13.17        | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
   13.18        | _ => Thm.dest_fun2 tm)
   13.19      and find_args bounds tm =
   13.20 @@ -230,7 +230,7 @@
   13.21  
   13.22  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   13.23    let
   13.24 -    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   13.25 +    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
   13.26      fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
   13.27      val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   13.28      val p' = fold_rev gen ts p
    14.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 21 15:36:00 2014 +0000
    14.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 21 20:39:54 2014 +0100
    14.3 @@ -112,7 +112,7 @@
    14.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    14.5      (* The result of the quantifier elimination *)
    14.6      val (th, tac) = case (prop_of pre_thm) of
    14.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    14.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    14.9      let val pth =
   14.10            (* If quick_and_dirty then run without proof generation as oracle*)
   14.11               if Config.get ctxt quick_and_dirty
    15.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 21 15:36:00 2014 +0000
    15.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 21 20:39:54 2014 +0100
    15.3 @@ -143,7 +143,7 @@
    15.4          case lhs of
    15.5            Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
    15.6              mk_eqn (f, big_lambda x rhs)
    15.7 -        | f $ Const (@{const_name TYPE}, T) =>
    15.8 +        | f $ Const (@{const_name Pure.type}, T) =>
    15.9              mk_eqn (f, Abs ("t", T, rhs))
   15.10          | Const _ => Logic.mk_equals (lhs, rhs)
   15.11          | _ => raise TERM ("lhs not of correct form", [lhs, rhs])
    16.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Mar 21 15:36:00 2014 +0000
    16.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Mar 21 20:39:54 2014 +0100
    16.3 @@ -80,7 +80,7 @@
    16.4      val transformed_decls = map (transform thy) contconst_decls
    16.5    in
    16.6      thy
    16.7 -    |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
    16.8 +    |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
    16.9      |> Sign.add_trrules (maps #3 transformed_decls)
   16.10    end
   16.11  
    17.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Fri Mar 21 15:36:00 2014 +0000
    17.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Mar 21 20:39:54 2014 +0100
    17.3 @@ -12,10 +12,10 @@
    17.4  let
    17.5    val typ = Simple_Syntax.read_typ;
    17.6  in
    17.7 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    17.8 +  Sign.del_syntax (Symbol.xsymbolsN, false)
    17.9     [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
   17.10      ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
   17.11 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
   17.12 +  Sign.add_syntax (Symbol.xsymbolsN, false)
   17.13     [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
   17.14      ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
   17.15  end
    18.1 --- a/src/HOL/Import/import_rule.ML	Fri Mar 21 15:36:00 2014 +0000
    18.2 +++ b/src/HOL/Import/import_rule.ML	Fri Mar 21 20:39:54 2014 +0100
    18.3 @@ -172,7 +172,7 @@
    18.4    let
    18.5      val rhs = term_of rhs
    18.6      val typ = type_of rhs
    18.7 -    val thy1 = Sign.add_consts_i [(Binding.name constname, typ, NoSyn)] thy
    18.8 +    val thy1 = Sign.add_consts [(Binding.name constname, typ, NoSyn)] thy
    18.9      val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs)
   18.10      val (thms, thy2) = Global_Theory.add_defs false
   18.11        [((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1
    19.1 --- a/src/HOL/Library/Countable.thy	Fri Mar 21 15:36:00 2014 +0000
    19.2 +++ b/src/HOL/Library/Countable.thy	Fri Mar 21 20:39:54 2014 +0100
    19.3 @@ -275,7 +275,7 @@
    19.4        let
    19.5          val ty_name =
    19.6            (case goal of
    19.7 -            (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n
    19.8 +            (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n
    19.9            | _ => raise Match)
   19.10          val typedef_info = hd (Typedef.get_info ctxt ty_name)
   19.11          val typedef_thm = #type_definition (snd typedef_info)
    20.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Mar 21 15:36:00 2014 +0000
    20.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Mar 21 20:39:54 2014 +0100
    20.3 @@ -67,7 +67,7 @@
    20.4  
    20.5  (* THEOREMS *)
    20.6  notation (Rule output)
    20.7 -  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    20.8 +  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    20.9  
   20.10  syntax (Rule output)
   20.11    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   20.12 @@ -82,7 +82,7 @@
   20.13    "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
   20.14  
   20.15  notation (IfThen output)
   20.16 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   20.17 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   20.18  syntax (IfThen output)
   20.19    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   20.20    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   20.21 @@ -90,7 +90,7 @@
   20.22    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
   20.23  
   20.24  notation (IfThenNoBox output)
   20.25 -  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   20.26 +  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   20.27  syntax (IfThenNoBox output)
   20.28    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   20.29    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    21.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 15:36:00 2014 +0000
    21.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 20:39:54 2014 +0100
    21.3 @@ -33,7 +33,7 @@
    21.4  (* aligning equations *)
    21.5  notation (tab output)
    21.6    "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    21.7 -  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    21.8 +  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    21.9  
   21.10  (* Let *)
   21.11  translations 
    22.1 --- a/src/HOL/Library/bnf_decl.ML	Fri Mar 21 15:36:00 2014 +0000
    22.2 +++ b/src/HOL/Library/bnf_decl.ML	Fri Mar 21 20:39:54 2014 +0100
    22.3 @@ -57,7 +57,7 @@
    22.4        (if nwits = 1 then [0] else 1 upto nwits);
    22.5  
    22.6      val lthy = Local_Theory.background_theory
    22.7 -      (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    22.8 +      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    22.9          map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
   22.10          map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
   22.11        lthy;
    23.1 --- a/src/HOL/Library/refute.ML	Fri Mar 21 15:36:00 2014 +0000
    23.2 +++ b/src/HOL/Library/refute.ML	Fri Mar 21 20:39:54 2014 +0100
    23.3 @@ -545,10 +545,10 @@
    23.4      fun unfold_loop t =
    23.5        case t of
    23.6        (* Pure *)
    23.7 -        Const (@{const_name all}, _) => t
    23.8 -      | Const (@{const_name "=="}, _) => t
    23.9 -      | Const (@{const_name "==>"}, _) => t
   23.10 -      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
   23.11 +        Const (@{const_name Pure.all}, _) => t
   23.12 +      | Const (@{const_name Pure.eq}, _) => t
   23.13 +      | Const (@{const_name Pure.imp}, _) => t
   23.14 +      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
   23.15        (* HOL *)
   23.16        | Const (@{const_name Trueprop}, _) => t
   23.17        | Const (@{const_name Not}, _) => t
   23.18 @@ -709,11 +709,11 @@
   23.19      and collect_term_axioms t axs =
   23.20        case t of
   23.21        (* Pure *)
   23.22 -        Const (@{const_name all}, _) => axs
   23.23 -      | Const (@{const_name "=="}, _) => axs
   23.24 -      | Const (@{const_name "==>"}, _) => axs
   23.25 +        Const (@{const_name Pure.all}, _) => axs
   23.26 +      | Const (@{const_name Pure.eq}, _) => axs
   23.27 +      | Const (@{const_name Pure.imp}, _) => axs
   23.28        (* axiomatic type classes *)
   23.29 -      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
   23.30 +      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
   23.31        (* HOL *)
   23.32        | Const (@{const_name Trueprop}, _) => axs
   23.33        | Const (@{const_name Not}, _) => axs
   23.34 @@ -1183,7 +1183,7 @@
   23.35      (* interpretation which includes values for the (formerly)           *)
   23.36      (* quantified variables.                                             *)
   23.37      (* maps  !!x1...xn. !xk...xm. t   to   t  *)
   23.38 -    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
   23.39 +    fun strip_all_body (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) =
   23.40            strip_all_body t
   23.41        | strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
   23.42            strip_all_body t
   23.43 @@ -1191,7 +1191,7 @@
   23.44            strip_all_body t
   23.45        | strip_all_body t = t
   23.46      (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)
   23.47 -    fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
   23.48 +    fun strip_all_vars (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) =
   23.49            (a, T) :: strip_all_vars t
   23.50        | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) =
   23.51            strip_all_vars t
   23.52 @@ -1569,7 +1569,7 @@
   23.53  
   23.54  fun Pure_interpreter ctxt model args t =
   23.55    case t of
   23.56 -    Const (@{const_name all}, _) $ t1 =>
   23.57 +    Const (@{const_name Pure.all}, _) $ t1 =>
   23.58        let
   23.59          val (i, m, a) = interpret ctxt model args t1
   23.60        in
   23.61 @@ -1584,11 +1584,11 @@
   23.62              end
   23.63          | _ =>
   23.64            raise REFUTE ("Pure_interpreter",
   23.65 -            "\"all\" is followed by a non-function")
   23.66 +            "\"Pure.all\" is followed by a non-function")
   23.67        end
   23.68 -  | Const (@{const_name all}, _) =>
   23.69 +  | Const (@{const_name Pure.all}, _) =>
   23.70        SOME (interpret ctxt model args (eta_expand t 1))
   23.71 -  | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   23.72 +  | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
   23.73        let
   23.74          val (i1, m1, a1) = interpret ctxt model args t1
   23.75          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   23.76 @@ -1597,11 +1597,11 @@
   23.77          SOME ((if #def_eq args then make_def_equality else make_equality)
   23.78            (i1, i2), m2, a2)
   23.79        end
   23.80 -  | Const (@{const_name "=="}, _) $ _ =>
   23.81 +  | Const (@{const_name Pure.eq}, _) $ _ =>
   23.82        SOME (interpret ctxt model args (eta_expand t 1))
   23.83 -  | Const (@{const_name "=="}, _) =>
   23.84 +  | Const (@{const_name Pure.eq}, _) =>
   23.85        SOME (interpret ctxt model args (eta_expand t 2))
   23.86 -  | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
   23.87 +  | Const (@{const_name Pure.imp}, _) $ t1 $ t2 =>
   23.88        (* 3-valued logic *)
   23.89        let
   23.90          val (i1, m1, a1) = interpret ctxt model args t1
   23.91 @@ -1611,9 +1611,9 @@
   23.92        in
   23.93          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   23.94        end
   23.95 -  | Const (@{const_name "==>"}, _) $ _ =>
   23.96 +  | Const (@{const_name Pure.imp}, _) $ _ =>
   23.97        SOME (interpret ctxt model args (eta_expand t 1))
   23.98 -  | Const (@{const_name "==>"}, _) =>
   23.99 +  | Const (@{const_name Pure.imp}, _) =>
  23.100        SOME (interpret ctxt model args (eta_expand t 2))
  23.101    | _ => NONE;
  23.102  
  23.103 @@ -1632,7 +1632,7 @@
  23.104    (* redundant, since 'False' is also an IDT constructor *)
  23.105    | Const (@{const_name False}, _) =>
  23.106        SOME (FF, model, args)
  23.107 -  | Const (@{const_name All}, _) $ t1 =>  (* similar to "all" (Pure) *)
  23.108 +  | Const (@{const_name All}, _) $ t1 =>  (* similar to "Pure.all" *)
  23.109        let
  23.110          val (i, m, a) = interpret ctxt model args t1
  23.111        in
  23.112 @@ -1670,7 +1670,7 @@
  23.113        end
  23.114    | Const (@{const_name Ex}, _) =>
  23.115        SOME (interpret ctxt model args (eta_expand t 1))
  23.116 -  | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
  23.117 +  | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to Pure.eq *)
  23.118        let
  23.119          val (i1, m1, a1) = interpret ctxt model args t1
  23.120          val (i2, m2, a2) = interpret ctxt m1 a1 t2
  23.121 @@ -1715,7 +1715,7 @@
  23.122        (* this would make "undef" propagate, even for formulae like *)
  23.123        (* "True | undef":                                           *)
  23.124        (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
  23.125 -  | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
  23.126 +  | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to Pure.imp *)
  23.127        (* 3-valued logic *)
  23.128        let
  23.129          val (i1, m1, a1) = interpret ctxt model args t1
    24.1 --- a/src/HOL/List.thy	Fri Mar 21 15:36:00 2014 +0000
    24.2 +++ b/src/HOL/List.thy	Fri Mar 21 20:39:54 2014 +0100
    24.3 @@ -439,7 +439,7 @@
    24.4          val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
    24.5          val case2 =
    24.6            Syntax.const @{syntax_const "_case1"} $
    24.7 -            Syntax.const @{const_syntax dummy_pattern} $ NilC;
    24.8 +            Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC;
    24.9          val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   24.10        in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;
   24.11  
    25.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Mar 21 15:36:00 2014 +0000
    25.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Mar 21 20:39:54 2014 +0100
    25.3 @@ -435,7 +435,8 @@
    25.4               val ty = type_of a
    25.5               val (encoding, a) = remove_types encoding a
    25.6               val (encoding, b) = remove_types encoding b
    25.7 -             val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding 
    25.8 +             val (eq, encoding) =
    25.9 +              Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding 
   25.10           in
   25.11               (encoding, EqPrem (a, b, ty, eq))
   25.12           end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
    26.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 15:36:00 2014 +0000
    26.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 20:39:54 2014 +0100
    26.3 @@ -218,7 +218,7 @@
    26.4    (@{const_name induct_conj}, "'a"),*)
    26.5    (@{const_name "undefined"}, "'a"),
    26.6    (@{const_name "default"}, "'a"),
    26.7 -  (@{const_name "dummy_pattern"}, "'a::{}"),
    26.8 +  (@{const_name "Pure.dummy_pattern"}, "'a::{}"),
    26.9    (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   26.10    (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   26.11    (@{const_name "top_fun_inst.top_fun"}, "'a"),
   26.12 @@ -234,7 +234,7 @@
   26.13    "nibble"]
   26.14  
   26.15  val forbidden_consts =
   26.16 - [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
   26.17 + [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
   26.18  
   26.19  fun is_forbidden_theorem (s, th) =
   26.20    let val consts = Term.add_const_names (prop_of th) [] in
   26.21 @@ -254,7 +254,7 @@
   26.22    "HOL.induct_forall",
   26.23   @{const_name undefined},
   26.24   @{const_name default},
   26.25 - @{const_name dummy_pattern},
   26.26 + @{const_name Pure.dummy_pattern},
   26.27   @{const_name "HOL.simp_implies"},
   26.28   @{const_name "bot_fun_inst.bot_fun"},
   26.29   @{const_name "top_fun_inst.top_fun"},
   26.30 @@ -275,7 +275,7 @@
   26.31   @{const_name Quickcheck_Random.catch_match},
   26.32   @{const_name Quickcheck_Exhaustive.unknown},
   26.33   @{const_name Num.Bit0}, @{const_name Num.Bit1}
   26.34 - (*@{const_name "==>"}, @{const_name "=="}*)]
   26.35 + (*@{const_name Pure.imp}, @{const_name Pure.eq}*)]
   26.36  
   26.37  val forbidden_mutant_consts =
   26.38    [
    27.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 15:36:00 2014 +0000
    27.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 20:39:54 2014 +0100
    27.3 @@ -292,7 +292,7 @@
    27.4  
    27.5  subsection {* Known Constants *}
    27.6  
    27.7 -lemma "x \<equiv> all \<Longrightarrow> False"
    27.8 +lemma "x \<equiv> Pure.all \<Longrightarrow> False"
    27.9  nitpick [card = 1, expect = genuine]
   27.10  nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   27.11  nitpick [card = 6, expect = genuine]
   27.12 @@ -306,15 +306,15 @@
   27.13  nitpick [expect = genuine]
   27.14  oops
   27.15  
   27.16 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   27.17 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   27.18  nitpick [expect = none]
   27.19  by auto
   27.20  
   27.21 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   27.22 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   27.23  nitpick [expect = genuine]
   27.24  oops
   27.25  
   27.26 -lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
   27.27 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Pure.all P \<equiv> Pure.all (\<lambda>x. P (I x))"
   27.28  nitpick [expect = none]
   27.29  by auto
   27.30  
    28.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Mar 21 15:36:00 2014 +0000
    28.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Mar 21 20:39:54 2014 +0100
    28.3 @@ -326,7 +326,7 @@
    28.4  nitpick [expect = genuine]
    28.5  oops
    28.6  
    28.7 -lemma "(x \<equiv> all) \<Longrightarrow> False"
    28.8 +lemma "(x \<equiv> Pure.all) \<Longrightarrow> False"
    28.9  nitpick [expect = genuine]
   28.10  oops
   28.11  
    29.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 21 15:36:00 2014 +0000
    29.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 21 20:39:54 2014 +0100
    29.3 @@ -761,7 +761,7 @@
    29.4            (Const (rep_name, T --> T') $ lhs, rhs));
    29.5          val def_name = (Long_Name.base_name cname) ^ "_def";
    29.6          val ([def_thm], thy') = thy |>
    29.7 -          Sign.add_consts_i [(cname', constrT, mx)] |>
    29.8 +          Sign.add_consts [(cname', constrT, mx)] |>
    29.9            (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
   29.10        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
   29.11  
   29.12 @@ -1993,7 +1993,7 @@
   29.13  
   29.14      val (reccomb_defs, thy12) =
   29.15        thy11
   29.16 -      |> Sign.add_consts_i (map (fn ((name, T), T') =>
   29.17 +      |> Sign.add_consts (map (fn ((name, T), T') =>
   29.18            (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
   29.19            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   29.20        |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    30.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 21 15:36:00 2014 +0000
    30.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 21 20:39:54 2014 +0100
    30.3 @@ -32,8 +32,8 @@
    30.4  
    30.5  fun unquantify t =
    30.6    let
    30.7 -    val (vs, Ts) = split_list (strip_qnt_vars "all" t);
    30.8 -    val body = strip_qnt_body "all" t;
    30.9 +    val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} t);
   30.10 +    val body = strip_qnt_body @{const_name Pure.all} t;
   30.11      val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
   30.12        (fn Free (v, _) => insert (op =) v | _ => I) body []))
   30.13    in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
    31.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Mar 21 15:36:00 2014 +0000
    31.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Mar 21 20:39:54 2014 +0100
    31.3 @@ -134,7 +134,7 @@
    31.4      val thy = Context.theory_of context
    31.5      val thms_to_be_added = (case (prop_of orig_thm) of
    31.6          (* case: eqvt-lemma is of the implicational form *)
    31.7 -        (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
    31.8 +        (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
    31.9            let
   31.10              val (pi,typi) = get_pi concl thy
   31.11            in
    32.1 --- a/src/HOL/Product_Type.thy	Fri Mar 21 15:36:00 2014 +0000
    32.2 +++ b/src/HOL/Product_Type.thy	Fri Mar 21 20:39:54 2014 +0100
    32.3 @@ -457,7 +457,7 @@
    32.4  ML {*
    32.5    (* replace parameters of product type by individual component parameters *)
    32.6    local (* filtering with exists_paired_all is an essential optimization *)
    32.7 -    fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
    32.8 +    fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
    32.9            can HOLogic.dest_prodT T orelse exists_paired_all t
   32.10        | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
   32.11        | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
    33.1 --- a/src/HOL/Prolog/prolog.ML	Fri Mar 21 15:36:00 2014 +0000
    33.2 +++ b/src/HOL/Prolog/prolog.ML	Fri Mar 21 20:39:54 2014 +0100
    33.3 @@ -13,9 +13,9 @@
    33.4      Const(@{const_name Trueprop},_)$t     => isD t
    33.5    | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
    33.6    | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
    33.7 -  | Const(   "==>",_)$l$r     => isG l andalso isD r
    33.8 +  | Const(@{const_name Pure.imp},_)$l$r     => isG l andalso isD r
    33.9    | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   33.10 -  | Const("all",_)$Abs(s,_,t) => isD t
   33.11 +  | Const(@{const_name Pure.all},_)$Abs(s,_,t) => isD t
   33.12    | Const(@{const_name HOL.disj},_)$_$_       => false
   33.13    | Const(@{const_name Ex} ,_)$_          => false
   33.14    | Const(@{const_name Not},_)$_          => false
   33.15 @@ -33,9 +33,9 @@
   33.16    | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
   33.17    | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
   33.18    | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   33.19 -  | Const(   "==>",_)$l$r     => isD l andalso isG r
   33.20 +  | Const(@{const_name Pure.imp},_)$l$r     => isD l andalso isG r
   33.21    | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   33.22 -  | Const("all",_)$Abs(_,_,t) => isG t
   33.23 +  | Const(@{const_name Pure.all},_)$Abs(_,_,t) => isG t
   33.24    | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
   33.25    | Const(@{const_name True},_)           => true
   33.26    | Const(@{const_name Not},_)$_          => false
   33.27 @@ -79,8 +79,8 @@
   33.28          |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   33.29          |   ap t                          =                         (0,false,t);
   33.30  (*
   33.31 -        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
   33.32 -        |   rep_goal (Const ("==>",_)$s$t)         =
   33.33 +        fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t
   33.34 +        |   rep_goal (Const (@{const_name Pure.imp},_)$s$t)         =
   33.35                          (case rep_goal t of (l,t) => (s::l,t))
   33.36          |   rep_goal t                             = ([]  ,t);
   33.37          val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
    34.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 21 15:36:00 2014 +0000
    34.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 21 20:39:54 2014 +0100
    34.3 @@ -1001,7 +1001,7 @@
    34.4    in
    34.5      (c,
    34.6       ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
    34.7 -      Sign.add_consts_i [(b, T, NoSyn)] thy))
    34.8 +      Sign.add_consts [(b, T, NoSyn)] thy))
    34.9    end;
   34.10  
   34.11  fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
    35.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Mar 21 15:36:00 2014 +0000
    35.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Mar 21 20:39:54 2014 +0100
    35.3 @@ -320,7 +320,7 @@
    35.4      |> apfst the_single
    35.5  end
    35.6  
    35.7 -(*like strip_top_All_vars but for "all" instead of "All"*)
    35.8 +(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*)
    35.9  fun strip_top_all_vars acc t =
   35.10    if Logic.is_all t then
   35.11      let
    36.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 15:36:00 2014 +0000
    36.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 20:39:54 2014 +0100
    36.3 @@ -1670,7 +1670,7 @@
    36.4     (* @{const_name HOL.not_equal}, *)
    36.5     @{const_name HOL.False},
    36.6     @{const_name HOL.True},
    36.7 -   @{const_name "==>"}]
    36.8 +   @{const_name Pure.imp}]
    36.9  
   36.10  fun strip_qtfrs_tac ctxt =
   36.11    REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))
    37.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 15:36:00 2014 +0000
    37.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 20:39:54 2014 +0100
    37.3 @@ -404,8 +404,9 @@
    37.4  (* These are ignored anyway by the relevance filter (unless they appear in
    37.5     higher-order places) but not by the monomorphizer. *)
    37.6  val atp_logical_consts =
    37.7 -  [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
    37.8 -   @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    37.9 +  [@{const_name Pure.prop}, @{const_name Pure.conjunction},
   37.10 +   @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq},
   37.11 +   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   37.12     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   37.13  
   37.14  (* These are either simplified away by "Meson.presimplify" (most of the time) or
   37.15 @@ -437,7 +438,7 @@
   37.16  val tvar_a = TVar tvar_a_z
   37.17  val tvar_a_name = tvar_name tvar_a_z
   37.18  val itself_name = `make_fixed_type_const @{type_name itself}
   37.19 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
   37.20 +val TYPE_name = `(make_fixed_const NONE) @{const_name Pure.type}
   37.21  val tvar_a_atype = AType ((tvar_a_name, []), [])
   37.22  val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
   37.23  
   37.24 @@ -1879,8 +1880,8 @@
   37.25    in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
   37.26  
   37.27  fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
   37.28 -  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
   37.29 -  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
   37.30 +  | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t
   37.31 +  | s_not_prop t = @{const Pure.imp} $ t $ @{prop False}
   37.32  
   37.33  fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
   37.34                         concl_t facts =
    38.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 15:36:00 2014 +0000
    38.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 20:39:54 2014 +0100
    38.3 @@ -46,7 +46,7 @@
    38.4  
    38.5  fun hhf_concl_conv cv ctxt ct =
    38.6    (case Thm.term_of ct of
    38.7 -    Const (@{const_name all}, _) $ Abs _ =>
    38.8 +    Const (@{const_name Pure.all}, _) $ Abs _ =>
    38.9      Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
   38.10    | _ => Conv.concl_conv ~1 cv ct);
   38.11  
    39.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Mar 21 15:36:00 2014 +0000
    39.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Mar 21 20:39:54 2014 +0100
    39.3 @@ -86,8 +86,8 @@
    39.4    | retype_free _ t = raise TERM ("retype_free", [t]);
    39.5  
    39.6  fun drop_all t =
    39.7 -  subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
    39.8 -    strip_qnt_body @{const_name all} t);
    39.9 +  subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
   39.10 +    strip_qnt_body @{const_name Pure.all} t);
   39.11  
   39.12  fun permute_args n t =
   39.13    list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
    40.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 21 15:36:00 2014 +0000
    40.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 21 20:39:54 2014 +0100
    40.3 @@ -149,7 +149,7 @@
    40.4            | abs_pat _ _ = I;
    40.5  
    40.6          (* replace occurrences of dummy_pattern by distinct variables *)
    40.7 -        fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
    40.8 +        fun replace_dummies (Const (@{const_syntax Pure.dummy_pattern}, T)) used =
    40.9                let val (x, used') = variant_free "x" used
   40.10                in (Free (x, T), used') end
   40.11            | replace_dummies (t $ u) used =
    41.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 21 15:36:00 2014 +0000
    41.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 21 20:39:54 2014 +0100
    41.3 @@ -237,7 +237,7 @@
    41.4            HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
    41.5          val ([def_thm], thy') =
    41.6            thy
    41.7 -          |> Sign.add_consts_i [(cname', constrT, mx)]
    41.8 +          |> Sign.add_consts [(cname', constrT, mx)]
    41.9            |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
   41.10  
   41.11        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
   41.12 @@ -262,7 +262,7 @@
   41.13      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
   41.14        fold dt_constr_defs
   41.15          (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax)
   41.16 -        (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
   41.17 +        (thy3 |> Sign.add_consts iso_decls |> Sign.parent_path, [], [], [], []);
   41.18  
   41.19  
   41.20      (*********** isomorphisms for new types (introduced by typedef) ***********)
    42.1 --- a/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 15:36:00 2014 +0000
    42.2 +++ b/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 20:39:54 2014 +0100
    42.3 @@ -34,8 +34,8 @@
    42.4  
    42.5  fun process_eqn is_fixed spec rec_fns =
    42.6    let
    42.7 -    val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
    42.8 -    val body = strip_qnt_body "all" spec;
    42.9 +    val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec);
   42.10 +    val body = strip_qnt_body @{const_name Pure.all} spec;
   42.11      val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
   42.12        (fn Free (v, _) => insert (op =) v | _ => I) body []));
   42.13      val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
    43.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 15:36:00 2014 +0000
    43.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 20:39:54 2014 +0100
    43.3 @@ -226,7 +226,7 @@
    43.4  
    43.5      val (reccomb_defs, thy2) =
    43.6        thy1
    43.7 -      |> Sign.add_consts_i (map (fn ((name, T), T') =>
    43.8 +      |> Sign.add_consts (map (fn ((name, T), T') =>
    43.9              (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
   43.10              (reccomb_names ~~ recTs ~~ rec_result_Ts))
   43.11        |> (Global_Theory.add_defs false o map Thm.no_attributes)
   43.12 @@ -434,7 +434,7 @@
   43.13    let
   43.14      fun prove_case_cong ((t, nchotomy), case_rewrites) =
   43.15        let
   43.16 -        val Const ("==>", _) $ tm $ _ = t;
   43.17 +        val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
   43.18          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
   43.19          val cert = cterm_of thy;
   43.20          val nchotomy' = nchotomy RS spec;
    44.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 15:36:00 2014 +0000
    44.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 21 20:39:54 2014 +0100
    44.3 @@ -280,8 +280,8 @@
    44.4  fun split_def ctxt check_head geq =
    44.5    let
    44.6      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
    44.7 -    val qs = Term.strip_qnt_vars "all" geq
    44.8 -    val imp = Term.strip_qnt_body "all" geq
    44.9 +    val qs = Term.strip_qnt_vars @{const_name Pure.all} geq
   44.10 +    val imp = Term.strip_qnt_body @{const_name Pure.all} geq
   44.11      val (gs, eq) = Logic.strip_horn imp
   44.12  
   44.13      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    45.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 15:36:00 2014 +0000
    45.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 20:39:54 2014 +0100
    45.3 @@ -40,7 +40,7 @@
    45.4  
    45.5  
    45.6  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    45.7 -fun dest_all_all (t as (Const ("all",_) $ _)) =
    45.8 +fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) =
    45.9    let
   45.10      val (v,b) = Logic.dest_all t |> apfst Free
   45.11      val (vs, b') = dest_all_all b
    46.1 --- a/src/HOL/Tools/Function/size.ML	Fri Mar 21 15:36:00 2014 +0000
    46.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Mar 21 20:39:54 2014 +0100
    46.3 @@ -134,7 +134,7 @@
    46.4  
    46.5      val ((size_def_thms, size_def_thms'), thy') =
    46.6        thy
    46.7 -      |> Sign.add_consts_i (map (fn (s, T) =>
    46.8 +      |> Sign.add_consts (map (fn (s, T) =>
    46.9             (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
   46.10             (size_names ~~ recTs1))
   46.11        |> Global_Theory.add_defs false
    47.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 15:36:00 2014 +0000
    47.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 20:39:54 2014 +0100
    47.3 @@ -547,11 +547,11 @@
    47.4  
    47.5  fun rename_to_tnames ctxt term =
    47.6    let
    47.7 -    fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t
    47.8 +    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
    47.9        | all_typs _ = []
   47.10  
   47.11 -    fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = 
   47.12 -        (Const ("all", T1) $ Abs (new_name, T2, rename t names)) 
   47.13 +    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   47.14 +        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   47.15        | rename t _ = t
   47.16  
   47.17      val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
    48.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 15:36:00 2014 +0000
    48.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 20:39:54 2014 +0100
    48.3 @@ -105,7 +105,7 @@
    48.4      try (fn () =>
    48.5        let val thy = theory_of_thm thA
    48.6            val tmA = concl_of thA
    48.7 -          val Const("==>",_) $ tmB $ _ = prop_of thB
    48.8 +          val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB
    48.9            val tenv =
   48.10              Pattern.first_order_match thy (tmB, tmA)
   48.11                                            (Vartab.empty, Vartab.empty) |> snd
   48.12 @@ -472,7 +472,7 @@
   48.13  
   48.14  (***** MESON PROOF PROCEDURE *****)
   48.15  
   48.16 -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   48.17 +fun rhyps (Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   48.18             As) = rhyps(phi, A::As)
   48.19    | rhyps (_, As) = As;
   48.20  
    49.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 15:36:00 2014 +0000
    49.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 20:39:54 2014 +0100
    49.3 @@ -242,7 +242,7 @@
    49.4      fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
    49.5        case t of
    49.6          (t1 as Const (s, _)) $ Abs (s', T, t') =>
    49.7 -        if s = @{const_name all} orelse s = @{const_name All} orelse
    49.8 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
    49.9             s = @{const_name Ex} then
   49.10            let
   49.11              val skolem = (pos = (s = @{const_name Ex}))
   49.12 @@ -254,7 +254,7 @@
   49.13          else
   49.14            t
   49.15        | (t1 as Const (s, _)) $ t2 $ t3 =>
   49.16 -        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
   49.17 +        if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then
   49.18            t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
   49.19          else if s = @{const_name HOL.conj} orelse
   49.20                  s = @{const_name HOL.disj} then
   49.21 @@ -275,13 +275,13 @@
   49.22    ct
   49.23    |> (case term_of ct of
   49.24          Const (s, _) $ Abs (s', _, _) =>
   49.25 -        if s = @{const_name all} orelse s = @{const_name All} orelse
   49.26 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
   49.27             s = @{const_name Ex} then
   49.28            Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
   49.29          else
   49.30            Conv.all_conv
   49.31        | Const (s, _) $ _ $ _ =>
   49.32 -        if s = @{const_name "==>"} orelse s = @{const_name implies} then
   49.33 +        if s = @{const_name Pure.imp} orelse s = @{const_name implies} then
   49.34            Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
   49.35          else if s = @{const_name conj} orelse s = @{const_name disj} then
   49.36            Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
    50.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 21 15:36:00 2014 +0000
    50.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 21 20:39:54 2014 +0100
    50.3 @@ -1062,7 +1062,7 @@
    50.4    end
    50.5  
    50.6  fun is_fixed_equation ctxt
    50.7 -                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
    50.8 +                      (Const (@{const_name Pure.eq}, _) $ Free (s, _) $ Const _) =
    50.9      Variable.is_fixed ctxt s
   50.10    | is_fixed_equation _ _ = false
   50.11  
    51.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 15:36:00 2014 +0000
    51.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 20:39:54 2014 +0100
    51.3 @@ -363,9 +363,9 @@
    51.4     "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
    51.5     well. *)
    51.6  val built_in_consts =
    51.7 -  [(@{const_name all}, 1),
    51.8 -   (@{const_name "=="}, 2),
    51.9 -   (@{const_name "==>"}, 2),
   51.10 +  [(@{const_name Pure.all}, 1),
   51.11 +   (@{const_name Pure.eq}, 2),
   51.12 +   (@{const_name Pure.imp}, 2),
   51.13     (@{const_name Pure.conjunction}, 2),
   51.14     (@{const_name Trueprop}, 1),
   51.15     (@{const_name Not}, 1),
   51.16 @@ -973,7 +973,7 @@
   51.17        fold (fn (z as ((s, _), T)) => fn t' =>
   51.18                 Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
   51.19             (take (length zs' - length zs) zs')
   51.20 -    fun aux zs (@{const "==>"} $ t1 $ t2) =
   51.21 +    fun aux zs (@{const Pure.imp} $ t1 $ t2) =
   51.22          let val zs' = Term.add_vars t1 zs in
   51.23            close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
   51.24          end
   51.25 @@ -1178,7 +1178,7 @@
   51.26    | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   51.27    | loose_bvar1_count _ = 0
   51.28  
   51.29 -fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) =
   51.30 +fun s_betapply _ (t1 as Const (@{const_name Pure.eq}, _) $ t1', t2) =
   51.31      if t1' aconv t2 then @{prop True} else t1 $ t2
   51.32    | s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) =
   51.33      if t1' aconv t2 then @{term True} else t1 $ t2
   51.34 @@ -1422,8 +1422,8 @@
   51.35     simplification rules (equational specifications). *)
   51.36  fun term_under_def t =
   51.37    case t of
   51.38 -    @{const "==>"} $ _ $ t2 => term_under_def t2
   51.39 -  | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
   51.40 +    @{const Pure.imp} $ _ $ t2 => term_under_def t2
   51.41 +  | Const (@{const_name Pure.eq}, _) $ t1 $ _ => term_under_def t1
   51.42    | @{const Trueprop} $ t1 => term_under_def t1
   51.43    | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
   51.44    | Abs (_, _, t') => term_under_def t'
   51.45 @@ -1444,11 +1444,11 @@
   51.46  fun normalized_rhs_of t =
   51.47    let
   51.48      fun aux (v as Var _) (SOME t) = SOME (lambda v t)
   51.49 -      | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
   51.50 +      | aux (c as Const (@{const_name Pure.type}, _)) (SOME t) = SOME (lambda c t)
   51.51        | aux _ _ = NONE
   51.52      val (lhs, rhs) =
   51.53        case t of
   51.54 -        Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
   51.55 +        Const (@{const_name Pure.eq}, _) $ t1 $ t2 => (t1, t2)
   51.56        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
   51.57          (t1, t2)
   51.58        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
   51.59 @@ -1527,9 +1527,9 @@
   51.60  
   51.61  fun lhs_of_equation t =
   51.62    case t of
   51.63 -    Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   51.64 -  | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
   51.65 -  | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
   51.66 +    Const (@{const_name Pure.all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   51.67 +  | Const (@{const_name Pure.eq}, _) $ t1 $ _ => SOME t1
   51.68 +  | @{const Pure.imp} $ _ $ t2 => lhs_of_equation t2
   51.69    | @{const Trueprop} $ t1 => lhs_of_equation t1
   51.70    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   51.71    | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
   51.72 @@ -1947,7 +1947,7 @@
   51.73            @{const Trueprop} $ extensional_equal j T t1 t2
   51.74          | @{const Trueprop} $ t' =>
   51.75            @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
   51.76 -        | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   51.77 +        | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   51.78            @{const Trueprop} $ extensional_equal j T t1 t2
   51.79          | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
   51.80                           quote (Syntax.string_of_term ctxt t) ^ ".");
    52.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 21 15:36:00 2014 +0000
    52.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 21 20:39:54 2014 +0100
    52.3 @@ -844,8 +844,8 @@
    52.4              if not (could_exist_alpha_subtype alpha_T T) then
    52.5                (mtype_for T, accum)
    52.6              else case s of
    52.7 -              @{const_name all} => do_all T accum
    52.8 -            | @{const_name "=="} => do_equals T accum
    52.9 +              @{const_name Pure.all} => do_all T accum
   52.10 +            | @{const_name Pure.eq} => do_equals T accum
   52.11              | @{const_name All} => do_all T accum
   52.12              | @{const_name Ex} =>
   52.13                let val set_T = domain_type T in
   52.14 @@ -1057,9 +1057,9 @@
   52.15                              " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   52.16                              " : o\<^sup>" ^ string_for_sign sn ^ "?");
   52.17          case t of
   52.18 -          Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
   52.19 +          Const (s as @{const_name Pure.all}, _) $ Abs (_, T1, t1) =>
   52.20            do_quantifier s T1 t1
   52.21 -        | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
   52.22 +        | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => do_equals t1 t2
   52.23          | @{const Trueprop} $ t1 => do_formula sn t1 accum
   52.24          | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
   52.25            do_quantifier s T1 t1
   52.26 @@ -1076,7 +1076,7 @@
   52.27            do_formula sn (betapply (t2, t1)) accum
   52.28          | @{const Pure.conjunction} $ t1 $ t2 =>
   52.29            do_connect meta_conj_spec false t1 t2 accum
   52.30 -        | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   52.31 +        | @{const Pure.imp} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   52.32          | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
   52.33          | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
   52.34          | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
   52.35 @@ -1122,11 +1122,11 @@
   52.36        and do_implies t1 t2 = do_term t1 #> do_formula t2
   52.37        and do_formula t accum =
   52.38          case t of
   52.39 -          Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   52.40 +          Const (@{const_name Pure.all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   52.41          | @{const Trueprop} $ t1 => do_formula t1 accum
   52.42 -        | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   52.43 +        | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
   52.44            consider_general_equals mdata true t1 t2 accum
   52.45 -        | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
   52.46 +        | @{const Pure.imp} $ t1 $ t2 => do_implies t1 t2 accum
   52.47          | @{const Pure.conjunction} $ t1 $ t2 =>
   52.48            fold (do_formula) [t1, t2] accum
   52.49          | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
    53.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Mar 21 15:36:00 2014 +0000
    53.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Mar 21 20:39:54 2014 +0100
    53.3 @@ -474,12 +474,12 @@
    53.4            | k => sub (eta_expand Ts t k)
    53.5        in
    53.6          case strip_comb t of
    53.7 -          (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
    53.8 +          (Const (@{const_name Pure.all}, _), [Abs (s, T, t1)]) =>
    53.9            do_quantifier All s T t1
   53.10 -        | (t0 as Const (@{const_name all}, _), [t1]) =>
   53.11 +        | (t0 as Const (@{const_name Pure.all}, _), [t1]) =>
   53.12            sub' (t0 $ eta_expand Ts t1 1)
   53.13 -        | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
   53.14 -        | (Const (@{const_name "==>"}, _), [t1, t2]) =>
   53.15 +        | (Const (@{const_name Pure.eq}, T), [t1, t2]) => sub_equals T t1 t2
   53.16 +        | (Const (@{const_name Pure.imp}, _), [t1, t2]) =>
   53.17            Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
   53.18          | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
   53.19            Op2 (And, prop_T, Any, sub' t1, sub' t2)
    54.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 15:36:00 2014 +0000
    54.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 20:39:54 2014 +0100
    54.3 @@ -36,9 +36,9 @@
    54.4  
    54.5  val may_use_binary_ints =
    54.6    let
    54.7 -    fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
    54.8 +    fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) =
    54.9          aux def t1 andalso aux false t2
   54.10 -      | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
   54.11 +      | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def t2
   54.12        | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
   54.13          aux def t1 andalso aux false t2
   54.14        | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
   54.15 @@ -145,7 +145,7 @@
   54.16        case t of
   54.17          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   54.18        | Const (s0, _) $ t1 $ _ =>
   54.19 -        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
   54.20 +        if s0 = @{const_name Pure.eq} orelse s0 = @{const_name HOL.eq} then
   54.21            let
   54.22              val (t', args) = strip_comb t1
   54.23              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   54.24 @@ -187,12 +187,12 @@
   54.25        end
   54.26      and do_term new_Ts old_Ts polar t =
   54.27        case t of
   54.28 -        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   54.29 +        Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   54.30          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   54.31 -      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
   54.32 +      | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 =>
   54.33          do_equals new_Ts old_Ts s0 T0 t1 t2
   54.34 -      | @{const "==>"} $ t1 $ t2 =>
   54.35 -        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   54.36 +      | @{const Pure.imp} $ t1 $ t2 =>
   54.37 +        @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   54.38          $ do_term new_Ts old_Ts polar t2
   54.39        | @{const Pure.conjunction} $ t1 $ t2 =>
   54.40          @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
   54.41 @@ -334,9 +334,9 @@
   54.42      val k = maxidx_of_term t + 1
   54.43      fun do_term Ts def t args seen =
   54.44        case t of
   54.45 -        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
   54.46 +        (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 =>
   54.47          do_eq_or_imp Ts true def t0 t1 t2 seen
   54.48 -      | (t0 as @{const "==>"}) $ t1 $ t2 =>
   54.49 +      | (t0 as @{const Pure.imp}) $ t1 $ t2 =>
   54.50          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   54.51        | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   54.52          do_eq_or_imp Ts true def t0 t1 t2 seen
   54.53 @@ -401,9 +401,9 @@
   54.54      val num_occs_of_var =
   54.55        fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   54.56                      | _ => I) t (K 0)
   54.57 -    fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
   54.58 +    fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) =
   54.59          aux_eq Ts careful true t0 t1 t2
   54.60 -      | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
   54.61 +      | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) =
   54.62          t0 $ aux Ts false t1 $ aux Ts careful t2
   54.63        | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
   54.64          aux_eq Ts careful true t0 t1 t2
   54.65 @@ -455,22 +455,22 @@
   54.66  
   54.67  (** Destruction of universal and existential equalities **)
   54.68  
   54.69 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
   54.70 +fun curry_assms (@{const Pure.imp} $ (@{const Trueprop}
   54.71                                     $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
   54.72      curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   54.73 -  | curry_assms (@{const "==>"} $ t1 $ t2) =
   54.74 -    @{const "==>"} $ curry_assms t1 $ curry_assms t2
   54.75 +  | curry_assms (@{const Pure.imp} $ t1 $ t2) =
   54.76 +    @{const Pure.imp} $ curry_assms t1 $ curry_assms t2
   54.77    | curry_assms t = t
   54.78  
   54.79  val destroy_universal_equalities =
   54.80    let
   54.81      fun aux prems zs t =
   54.82        case t of
   54.83 -        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
   54.84 +        @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2
   54.85        | _ => Logic.list_implies (rev prems, t)
   54.86      and aux_implies prems zs t1 t2 =
   54.87        case t1 of
   54.88 -        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   54.89 +        Const (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   54.90        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
   54.91          aux_eq prems zs z t' t1 t2
   54.92        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
   54.93 @@ -591,10 +591,10 @@
   54.94                               not (is_higher_order_type abs_T)) polar t)
   54.95        in
   54.96          case t of
   54.97 -          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   54.98 +          Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   54.99            do_quantifier s0 T0 s1 T1 t1
  54.100 -        | @{const "==>"} $ t1 $ t2 =>
  54.101 -          @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
  54.102 +        | @{const Pure.imp} $ t1 $ t2 =>
  54.103 +          @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1
  54.104            $ aux ss Ts js skolemizable polar t2
  54.105          | @{const Pure.conjunction} $ t1 $ t2 =>
  54.106            @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
  54.107 @@ -654,7 +654,7 @@
  54.108  
  54.109  (** Function specialization **)
  54.110  
  54.111 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
  54.112 +fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2
  54.113    | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
  54.114    | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
  54.115      snd (strip_comb t1)
  54.116 @@ -866,7 +866,7 @@
  54.117        if exists_subterm (curry (op aconv) u) def then NONE else SOME u
  54.118    in
  54.119      case t of
  54.120 -      Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def
  54.121 +      Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def
  54.122      | @{const Trueprop}
  54.123        $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
  54.124        do_equals u def
  54.125 @@ -918,7 +918,7 @@
  54.126      and add_def_axiom depth = add_axiom fst apfst true depth
  54.127      and add_nondef_axiom depth = add_axiom snd apsnd false depth
  54.128      and add_maybe_def_axiom depth t =
  54.129 -      (if head_of t <> @{const "==>"} then add_def_axiom
  54.130 +      (if head_of t <> @{const Pure.imp} then add_def_axiom
  54.131         else add_nondef_axiom) depth t
  54.132      and add_eq_axiom depth t =
  54.133        (if is_constr_pattern_formula ctxt t then add_def_axiom
  54.134 @@ -979,7 +979,7 @@
  54.135                                              (Const (mate_of_rep_fun ctxt x))
  54.136                       |> fold (add_def_axiom depth)
  54.137                               (inverse_axioms_for_rep_fun ctxt x)
  54.138 -             else if s = @{const_name TYPE} then
  54.139 +             else if s = @{const_name Pure.type} then
  54.140                 accum
  54.141               else case def_of_const thy def_tables x of
  54.142                 SOME _ =>
    55.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 21 15:36:00 2014 +0000
    55.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 21 20:39:54 2014 +0100
    55.3 @@ -307,7 +307,8 @@
    55.4  
    55.5  fun imp_prems_conv cv ct =
    55.6    (case Thm.term_of ct of
    55.7 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    55.8 +    Const (@{const_name Pure.imp}, _) $ _ $ _ =>
    55.9 +      Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   55.10    | _ => Conv.all_conv ct)
   55.11  
   55.12  fun preprocess_intro thy rule =
    56.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 15:36:00 2014 +0000
    56.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 20:39:54 2014 +0100
    56.3 @@ -460,14 +460,14 @@
    56.4  
    56.5  (* general syntactic functions *)
    56.6  
    56.7 -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    56.8 +fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = true
    56.9    | is_equationlike_term
   56.10        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
   56.11    | is_equationlike_term _ = false
   56.12  
   56.13  val is_equationlike = is_equationlike_term o prop_of
   56.14  
   56.15 -fun is_pred_equation_term (Const ("==", _) $ u $ v) =
   56.16 +fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) =
   56.17        (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
   56.18    | is_pred_equation_term _ = false
   56.19  
   56.20 @@ -620,7 +620,7 @@
   56.21  (*
   56.22  fun equals_conv lhs_cv rhs_cv ct =
   56.23    case Thm.term_of ct of
   56.24 -    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
   56.25 +    Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct
   56.26    | _ => error "equals_conv"
   56.27  *)
   56.28  
   56.29 @@ -973,7 +973,8 @@
   56.30  
   56.31  fun imp_prems_conv cv ct =
   56.32    (case Thm.term_of ct of
   56.33 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   56.34 +    Const (@{const_name Pure.imp}, _) $ _ $ _ =>
   56.35 +      Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   56.36    | _ => Conv.all_conv ct)
   56.37  
   56.38  
   56.39 @@ -1212,7 +1213,7 @@
   56.40      val constname = "quickcheck"
   56.41      val full_constname = Sign.full_bname thy constname
   56.42      val constT = map snd vs' ---> @{typ bool}
   56.43 -    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
   56.44 +    val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy
   56.45      val const = Const (full_constname, constT)
   56.46      val t =
   56.47        Logic.list_implies
    57.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 21 15:36:00 2014 +0000
    57.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 21 20:39:54 2014 +0100
    57.3 @@ -1146,7 +1146,7 @@
    57.4          val lhs = Const (mode_cname, funT)
    57.5          val def = Logic.mk_equals (lhs, predterm)
    57.6          val ([definition], thy') = thy |>
    57.7 -          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
    57.8 +          Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
    57.9            Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
   57.10          val ctxt' = Proof_Context.init_global thy'
   57.11          val rules as ((intro, elim), _) =
   57.12 @@ -1171,7 +1171,7 @@
   57.13          val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
   57.14          val funT = Comp_Mod.funT_of comp_modifiers mode T
   57.15        in
   57.16 -        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
   57.17 +        thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
   57.18          |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
   57.19        end;
   57.20    in
    58.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 21 15:36:00 2014 +0000
    58.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 21 20:39:54 2014 +0100
    58.3 @@ -84,7 +84,7 @@
    58.4  
    58.5  val is_introlike = is_introlike_term o prop_of
    58.6  
    58.7 -fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
    58.8 +fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) =
    58.9        (case strip_comb u of
   58.10          (Const (_, T), args) =>
   58.11            if (length (binder_types T) = length args) then
   58.12 @@ -98,7 +98,7 @@
   58.13  val check_equation_format = check_equation_format_term o prop_of
   58.14  
   58.15  
   58.16 -fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
   58.17 +fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u)
   58.18    | defining_term_of_equation_term t =
   58.19        raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
   58.20  
   58.21 @@ -224,8 +224,8 @@
   58.22    end
   58.23  
   58.24  val logic_operator_names =
   58.25 -  [@{const_name "=="},
   58.26 -   @{const_name "==>"},
   58.27 +  [@{const_name Pure.eq},
   58.28 +   @{const_name Pure.imp},
   58.29     @{const_name Trueprop},
   58.30     @{const_name Not},
   58.31     @{const_name HOL.eq},
    59.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Mar 21 15:36:00 2014 +0000
    59.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Mar 21 20:39:54 2014 +0100
    59.3 @@ -284,7 +284,7 @@
    59.4            end
    59.5        val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
    59.6        val (intrs, thy') = thy
    59.7 -        |> Sign.add_consts_i
    59.8 +        |> Sign.add_consts
    59.9            (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
   59.10             dst_preds)
   59.11          |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
    60.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 21 15:36:00 2014 +0000
    60.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 21 20:39:54 2014 +0100
    60.3 @@ -87,7 +87,7 @@
    60.4        val lhs = list_comb (Const (full_constname, constT), params @ args)
    60.5        val def = Logic.mk_equals (lhs, atom)
    60.6        val ([definition], thy') = thy
    60.7 -        |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    60.8 +        |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
    60.9          |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
   60.10      in
   60.11        (lhs, ((full_constname, [definition]) :: defs, thy'))
   60.12 @@ -119,7 +119,7 @@
   60.13                  Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
   60.14                val new_defs = map mk_def srs
   60.15                val (definition, thy') = thy
   60.16 -              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   60.17 +              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
   60.18                |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
   60.19                  (map_index (fn (i, t) =>
   60.20                    ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
   60.21 @@ -245,7 +245,7 @@
   60.22              val lhs = list_comb (const, frees)
   60.23              val def = Logic.mk_equals (lhs, abs_arg')
   60.24              val ([definition], thy') = thy
   60.25 -              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   60.26 +              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
   60.27                |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
   60.28            in
   60.29              (list_comb (Logic.varify_global const, vars),
    61.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Mar 21 15:36:00 2014 +0000
    61.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Mar 21 20:39:54 2014 +0100
    61.3 @@ -94,7 +94,7 @@
    61.4        end handle Pattern.Unif => NONE)
    61.5      val specialised_intros_t = map_filter I (map specialise_intro intros)
    61.6      val thy' =
    61.7 -      Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
    61.8 +      Sign.add_consts [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
    61.9      val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
   61.10      val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
   61.11      val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
    62.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Mar 21 15:36:00 2014 +0000
    62.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Mar 21 20:39:54 2014 +0100
    62.3 @@ -795,7 +795,7 @@
    62.4  
    62.5  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    62.6   let 
    62.7 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    62.8 +   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
    62.9     fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
   62.10     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   62.11     val p' = fold_rev gen ts p
    63.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 21 15:36:00 2014 +0000
    63.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 21 20:39:54 2014 +0100
    63.3 @@ -428,7 +428,7 @@
    63.4  fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = 
    63.5    let
    63.6      val frees = Term.add_free_names t []
    63.7 -    val dummy_term = @{term "Code_Evaluation.Const (STR ''dummy_pattern'')
    63.8 +    val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'')
    63.9        (Typerep.Typerep (STR ''dummy'') [])"}
   63.10      val return = @{term "Some :: term list => term list option"} $
   63.11        (HOLogic.mk_list @{typ "term"}
    64.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 21 15:36:00 2014 +0000
    64.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 21 20:39:54 2014 +0100
    64.3 @@ -34,7 +34,7 @@
    64.4  fun mk_partial_term_of (x, T) =
    64.5    Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
    64.6      Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
    64.7 -      $ Const ("TYPE", Term.itselfT T) $ x
    64.8 +      $ Logic.mk_type T $ x
    64.9  
   64.10  (** formal definition **)
   64.11  
    65.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 15:36:00 2014 +0000
    65.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 20:39:54 2014 +0100
    65.3 @@ -52,7 +52,7 @@
    65.4    (case Thm.prop_of thm of
    65.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    65.6        norm_def (thm RS @{thm fun_cong})
    65.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    65.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
    65.9        norm_def (thm RS @{thm meta_eq_to_obj_eq})
   65.10    | _ => thm)
   65.11  
   65.12 @@ -61,20 +61,20 @@
   65.13  
   65.14  fun atomize_conv ctxt ct =
   65.15    (case Thm.term_of ct of
   65.16 -    @{const "==>"} $ _ $ _ =>
   65.17 +    @{const Pure.imp} $ _ $ _ =>
   65.18        Conv.binop_conv (atomize_conv ctxt) then_conv
   65.19        Conv.rewr_conv @{thm atomize_imp}
   65.20 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
   65.21 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   65.22        Conv.binop_conv (atomize_conv ctxt) then_conv
   65.23        Conv.rewr_conv @{thm atomize_eq}
   65.24 -  | Const (@{const_name all}, _) $ Abs _ =>
   65.25 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
   65.26        Conv.binder_conv (atomize_conv o snd) ctxt then_conv
   65.27        Conv.rewr_conv @{thm atomize_all}
   65.28    | _ => Conv.all_conv) ct
   65.29  
   65.30  val setup_atomize =
   65.31 -  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
   65.32 -    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
   65.33 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
   65.34 +    @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
   65.35  
   65.36  
   65.37  (** unfold special quantifiers **)
    66.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Fri Mar 21 15:36:00 2014 +0000
    66.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Fri Mar 21 20:39:54 2014 +0100
    66.3 @@ -188,7 +188,7 @@
    66.4      @{const Trueprop} $ _ => Thm.dest_arg ct
    66.5    | _ => raise CTERM ("not a property", [ct]))
    66.6  
    66.7 -val equals = mk_const_pat @{theory} @{const_name "=="} destT1
    66.8 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
    66.9  fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
   66.10  
   66.11  val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    67.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Mar 21 15:36:00 2014 +0000
    67.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Mar 21 20:39:54 2014 +0100
    67.3 @@ -614,7 +614,7 @@
    67.4  (* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
    67.5  local
    67.6    val forall =
    67.7 -    SMT_Utils.mk_const_pat @{theory} @{const_name all}
    67.8 +    SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all}
    67.9        (SMT_Utils.destT1 o SMT_Utils.destT1)
   67.10    fun mk_forall cv ct =
   67.11      Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
    68.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 15:36:00 2014 +0000
    68.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 20:39:54 2014 +0100
    68.3 @@ -199,7 +199,7 @@
    68.4      and abstr (dcvs as (d, cvs)) ct =
    68.5        (case Thm.term_of ct of
    68.6          @{const Trueprop} $ _ => abstr1 dcvs ct
    68.7 -      | @{const "==>"} $ _ $ _ => abstr2 dcvs ct
    68.8 +      | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
    68.9        | @{const True} => pair ct
   68.10        | @{const False} => pair ct
   68.11        | @{const Not} $ _ => abstr1 dcvs ct
   68.12 @@ -229,7 +229,7 @@
   68.13              | _ => fresh_abstraction dcvs ct cx)))
   68.14    in abstr (depth, []) end
   68.15  
   68.16 -val cimp = Thm.cterm_of @{theory} @{const "==>"}
   68.17 +val cimp = Thm.cterm_of @{theory} @{const Pure.imp}
   68.18  
   68.19  fun deepen depth f x =
   68.20    if depth = 0 then f depth x
    69.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 15:36:00 2014 +0000
    69.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 20:39:54 2014 +0100
    69.3 @@ -48,7 +48,7 @@
    69.4    (case Thm.prop_of thm of
    69.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    69.6        norm_def (thm RS @{thm fun_cong})
    69.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    69.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    69.9    | _ => thm)
   69.10  
   69.11  
   69.12 @@ -56,17 +56,17 @@
   69.13  
   69.14  fun atomize_conv ctxt ct =
   69.15    (case Thm.term_of ct of
   69.16 -    @{const "==>"} $ _ $ _ =>
   69.17 +    @{const Pure.imp} $ _ $ _ =>
   69.18        Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
   69.19 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
   69.20 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   69.21        Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
   69.22 -  | Const (@{const_name all}, _) $ Abs _ =>
   69.23 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
   69.24        Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
   69.25    | _ => Conv.all_conv) ct
   69.26  
   69.27  val setup_atomize =
   69.28 -  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
   69.29 -    @{const_name all}, @{const_name Trueprop}]
   69.30 +  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
   69.31 +    @{const_name Pure.all}, @{const_name Trueprop}]
   69.32  
   69.33  
   69.34  (** unfold special quantifiers **)
    70.1 --- a/src/HOL/Tools/SMT2/smt2_util.ML	Fri Mar 21 15:36:00 2014 +0000
    70.2 +++ b/src/HOL/Tools/SMT2/smt2_util.ML	Fri Mar 21 20:39:54 2014 +0100
    70.3 @@ -185,7 +185,7 @@
    70.4      @{const Trueprop} $ _ => Thm.dest_arg ct
    70.5    | _ => raise CTERM ("not a property", [ct]))
    70.6  
    70.7 -val equals = mk_const_pat @{theory} @{const_name "=="} destT1
    70.8 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
    70.9  fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
   70.10  
   70.11  val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    71.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 15:36:00 2014 +0000
    71.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 20:39:54 2014 +0100
    71.3 @@ -463,7 +463,7 @@
    71.4      val match = Sign.typ_match (Proof_Context.theory_of ctxt)
    71.5  
    71.6      val t' = singleton (Variable.polymorphic ctxt) t
    71.7 -    val patTs = map snd (Term.strip_qnt_vars @{const_name all} t')
    71.8 +    val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
    71.9      val objTs = map (the o Symtab.lookup env) bounds
   71.10      val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   71.11    in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
   71.12 @@ -501,7 +501,7 @@
   71.13      SOME (tyenv, _) => subst_of tyenv
   71.14    | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
   71.15  
   71.16 -fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) =
   71.17 +fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
   71.18        dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
   71.19    | dest_all i t = (i, t)
   71.20  
   71.21 @@ -517,7 +517,7 @@
   71.22      | SOME subst =>
   71.23          let
   71.24            val applyT = Same.commit (substTs_same subst)
   71.25 -          val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'')
   71.26 +          val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
   71.27          in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
   71.28    end
   71.29  
    72.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Fri Mar 21 15:36:00 2014 +0000
    72.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Fri Mar 21 20:39:54 2014 +0100
    72.3 @@ -14,7 +14,7 @@
    72.4  structure Z3_New_Replay: Z3_NEW_REPLAY =
    72.5  struct
    72.6  
    72.7 -fun params_of t = Term.strip_qnt_vars @{const_name all} t
    72.8 +fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t
    72.9  
   72.10  fun varify ctxt thm =
   72.11    let
   72.12 @@ -32,7 +32,7 @@
   72.13      fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
   72.14    in (ctxt', Symtab.make (map2 mk nTs ns)) end
   72.15  
   72.16 -fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
   72.17 +fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
   72.18        Term.betapply (a, Thm.term_of ct)
   72.19    | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
   72.20  
    73.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 21 15:36:00 2014 +0000
    73.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 21 20:39:54 2014 +0100
    73.3 @@ -85,8 +85,8 @@
    73.4  
    73.5  fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    73.6  fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    73.7 -  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    73.8 -  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    73.9 +  | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
   73.10 +  | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   73.11    | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   73.12    | is_rec_def _ = false
   73.13  
   73.14 @@ -260,13 +260,13 @@
   73.15        else
   73.16          Interesting
   73.17      fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
   73.18 -      | interest_of_prop Ts (@{const "==>"} $ t $ u) =
   73.19 +      | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
   73.20          combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
   73.21 -      | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   73.22 +      | interest_of_prop Ts (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
   73.23          if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
   73.24 -      | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   73.25 +      | interest_of_prop Ts ((t as Const (@{const_name Pure.all}, _)) $ u) =
   73.26          interest_of_prop Ts (t $ eta_expand Ts u 1)
   73.27 -      | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   73.28 +      | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
   73.29          combine_interests (interest_of_bool t) (interest_of_bool u)
   73.30        | interest_of_prop _ _ = Deal_Breaker
   73.31      val t = prop_of th
   73.32 @@ -351,7 +351,7 @@
   73.33    | normalize_eq (@{const Trueprop} $ (t as @{const Not}
   73.34          $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   73.35      if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
   73.36 -  | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   73.37 +  | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
   73.38      (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
   73.39      |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
   73.40    | normalize_eq t = t
    74.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Mar 21 15:36:00 2014 +0000
    74.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Mar 21 20:39:54 2014 +0100
    74.3 @@ -187,9 +187,9 @@
    74.4        if T = HOLogic.boolT then do_formula else do_term ext_arg
    74.5      and do_formula t =
    74.6        (case t of
    74.7 -        Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
    74.8 -      | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
    74.9 -      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   74.10 +        Const (@{const_name Pure.all}, _) $ Abs (_, _, t') => do_formula t'
   74.11 +      | @{const Pure.imp} $ t1 $ t2 => do_formula t1 #> do_formula t2
   74.12 +      | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   74.13          do_term_or_formula false T t1 #> do_term_or_formula true T t2
   74.14        | @{const Trueprop} $ t1 => do_formula t1
   74.15        | @{const False} => I
    75.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 21 15:36:00 2014 +0000
    75.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 21 20:39:54 2014 +0100
    75.3 @@ -77,10 +77,10 @@
    75.4      fun do_formula pos t =
    75.5        (case (pos, t) of
    75.6          (_, @{const Trueprop} $ t1) => do_formula pos t1
    75.7 -      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t'
    75.8 +      | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t'
    75.9        | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
   75.10        | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
   75.11 -      | (_, @{const "==>"} $ t1 $ t2) =>
   75.12 +      | (_, @{const Pure.imp} $ t1 $ t2) =>
   75.13          do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
   75.14        | (_, @{const HOL.implies} $ t1 $ t2) =>
   75.15          do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
   75.16 @@ -88,7 +88,7 @@
   75.17        | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   75.18        | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   75.19        | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   75.20 -      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   75.21 +      | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2
   75.22        | _ => false)
   75.23    in do_formula true end
   75.24  
    76.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Mar 21 15:36:00 2014 +0000
    76.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 21 20:39:54 2014 +0100
    76.3 @@ -63,7 +63,7 @@
    76.4     
    76.5  val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
    76.6  fun mk_meta_eq r = case concl_of r of
    76.7 -     Const("==",_)$_$_ => r
    76.8 +     Const(@{const_name Pure.eq},_)$_$_ => r
    76.9    |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
   76.10    |   _ => r RS P_imp_P_eq_True
   76.11  
    77.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Mar 21 15:36:00 2014 +0000
    77.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Mar 21 20:39:54 2014 +0100
    77.3 @@ -293,7 +293,7 @@
    77.4  fun GEN v th =
    77.5     let val gth = Thm.forall_intr v th
    77.6         val thy = Thm.theory_of_thm gth
    77.7 -       val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
    77.8 +       val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
    77.9         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   77.10         val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
   77.11         val allI2 = Drule.instantiate_normalize (certify thy theta) allI
   77.12 @@ -441,21 +441,22 @@
   77.13  
   77.14  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   77.15  fun is_cong thm =
   77.16 -  case (Thm.prop_of thm)
   77.17 -     of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
   77.18 -         (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
   77.19 -      | _ => true;
   77.20 +  case (Thm.prop_of thm) of
   77.21 +    (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
   77.22 +      (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) =>
   77.23 +        false
   77.24 +  | _ => true;
   77.25  
   77.26  
   77.27 -fun dest_equal(Const ("==",_) $
   77.28 +fun dest_equal(Const (@{const_name Pure.eq},_) $
   77.29                 (Const (@{const_name Trueprop},_) $ lhs)
   77.30                 $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
   77.31 -  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   77.32 +  | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
   77.33    | dest_equal tm = USyntax.dest_eq tm;
   77.34  
   77.35  fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   77.36  
   77.37 -fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
   77.38 +fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
   77.39    | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
   77.40  
   77.41  val is_all = can (dest_all []);
   77.42 @@ -468,10 +469,10 @@
   77.43          end
   77.44     else ([], fm, used);
   77.45  
   77.46 -fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   77.47 +fun break_all(Const(@{const_name Pure.all},_) $ Abs (_,_,body)) = body
   77.48    | break_all _ = raise RULES_ERR "break_all" "not a !!";
   77.49  
   77.50 -fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
   77.51 +fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
   77.52       let val (L,core) = list_break_all body
   77.53       in ((s,ty)::L, core)
   77.54       end
   77.55 @@ -725,7 +726,7 @@
   77.56  
   77.57               fun eliminate thm =
   77.58                 case Thm.prop_of thm
   77.59 -               of Const("==>",_) $ imp $ _ =>
   77.60 +               of Const(@{const_name Pure.imp},_) $ imp $ _ =>
   77.61                     eliminate
   77.62                      (if not(is_all imp)
   77.63                       then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
   77.64 @@ -740,7 +741,8 @@
   77.65                val cntxt = rev (Simplifier.prems_of ctxt)
   77.66                val dummy = print_thms ctxt "cntxt:" cntxt
   77.67                val thy = Thm.theory_of_thm thm
   77.68 -              val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
   77.69 +              val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
   77.70 +                Thm.prop_of thm
   77.71                fun genl tm = let val vlist = subtract (op aconv) globals
   77.72                                             (Misc_Legacy.add_term_frees(tm,[]))
   77.73                              in fold_rev Forall vlist tm
    78.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Mar 21 15:36:00 2014 +0000
    78.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Fri Mar 21 20:39:54 2014 +0100
    78.3 @@ -357,7 +357,7 @@
    78.4  (*For Isabelle, the lhs of a definition must be a constant.*)
    78.5  fun const_def sign (c, Ty, rhs) =
    78.6    singleton (Syntax.check_terms (Proof_Context.init_global sign))
    78.7 -    (Const("==",dummyT) $ Const(c,Ty) $ rhs);
    78.8 +    (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
    78.9  
   78.10  (*Make all TVars available for instantiation by adding a ? to the front*)
   78.11  fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
    79.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri Mar 21 15:36:00 2014 +0000
    79.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Mar 21 20:39:54 2014 +0100
    79.3 @@ -193,7 +193,7 @@
    79.4      val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    79.5      val t = Thm.term_of ct;
    79.6      val T = fastype_of t;
    79.7 -    val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
    79.8 +    val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
    79.9    in case value ctxt t
   79.10     of NONE => Thm.reflexive ct
   79.11      | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
   79.12 @@ -206,9 +206,9 @@
   79.13  
   79.14  fun static_conv ctxt consts Ts =
   79.15    let
   79.16 -    val eqs = "==" :: @{const_name HOL.eq} ::
   79.17 +    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
   79.18        map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
   79.19 -        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
   79.20 +        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
   79.21      val value = static_value ctxt consts Ts;
   79.22      val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
   79.23    in
    80.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 21 15:36:00 2014 +0000
    80.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 21 20:39:54 2014 +0100
    80.3 @@ -258,7 +258,7 @@
    80.4        handle THM _ => thm RS @{thm le_boolD}
    80.5    in
    80.6      (case concl_of thm of
    80.7 -      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
    80.8 +      Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
    80.9      | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
   80.10      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   80.11        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    81.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 15:36:00 2014 +0000
    81.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 20:39:54 2014 +0100
    81.3 @@ -31,20 +31,21 @@
    81.4  
    81.5  val pred_of = fst o dest_Const o head_of;
    81.6  
    81.7 -fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    81.8 +fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) =
    81.9        let val (s', names') = (case names of
   81.10            [] => (singleton (Name.variant_list used) s, [])
   81.11          | name :: names' => (name, names'))
   81.12        in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   81.13 -  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
   81.14 +  | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) =
   81.15        t $ strip_all' used names Q
   81.16    | strip_all' _ _ t = t;
   81.17  
   81.18  fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
   81.19  
   81.20 -fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
   81.21 +fun strip_one name
   81.22 +    (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) =
   81.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
   81.24 -  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
   81.25 +  | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q);
   81.26  
   81.27  fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
   81.28       (case strip_type T of
   81.29 @@ -145,8 +146,8 @@
   81.30  
   81.31      val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
   81.32  
   81.33 -    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   81.34 -      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   81.35 +    fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P
   81.36 +      | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
   81.37        | is_meta (Const (@{const_name Trueprop}, _) $ t) =
   81.38            (case head_of t of
   81.39              Const (s, _) => can (Inductive.the_inductive ctxt) s
    82.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Mar 21 15:36:00 2014 +0000
    82.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 21 20:39:54 2014 +0100
    82.3 @@ -50,7 +50,7 @@
    82.4                          addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
    82.5                      in
    82.6                        SOME (Goal.prove ctxt [] []
    82.7 -                        (Const ("==", T --> T --> propT) $ S $ S')
    82.8 +                        (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
    82.9                          (K (EVERY
   82.10                            [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
   82.11                             rtac subsetI 1, dtac CollectD 1, simp,
    83.1 --- a/src/HOL/Tools/record.ML	Fri Mar 21 15:36:00 2014 +0000
    83.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 21 20:39:54 2014 +0100
    83.3 @@ -1287,7 +1287,7 @@
    83.4      (fn ctxt => fn t =>
    83.5        (case t of
    83.6          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
    83.7 -          if quantifier = @{const_name all} orelse
    83.8 +          if quantifier = @{const_name Pure.all} orelse
    83.9              quantifier = @{const_name All} orelse
   83.10              quantifier = @{const_name Ex}
   83.11            then
   83.12 @@ -1301,7 +1301,7 @@
   83.13                      | SOME (all_thm, All_thm, Ex_thm, _) =>
   83.14                          SOME
   83.15                            (case quantifier of
   83.16 -                            @{const_name all} => all_thm
   83.17 +                            @{const_name Pure.all} => all_thm
   83.18                            | @{const_name All} => All_thm RS @{thm eq_reflection}
   83.19                            | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
   83.20                            | _ => raise Fail "split_simproc"))
   83.21 @@ -1368,8 +1368,8 @@
   83.22  
   83.23      val has_rec = exists_Const
   83.24        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   83.25 -          (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
   83.26 -          is_recT T
   83.27 +          (s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex})
   83.28 +            andalso is_recT T
   83.29          | _ => false);
   83.30  
   83.31      fun mk_split_free_tac free induct_thm i =
   83.32 @@ -1418,10 +1418,10 @@
   83.33  
   83.34      val has_rec = exists_Const
   83.35        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   83.36 -          (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
   83.37 +          (s = @{const_name Pure.all} orelse s = @{const_name All}) andalso is_recT T
   83.38          | _ => false);
   83.39  
   83.40 -    fun is_all (Const (@{const_name all}, _) $ _) = ~1
   83.41 +    fun is_all (Const (@{const_name Pure.all}, _) $ _) = ~1
   83.42        | is_all (Const (@{const_name All}, _) $ _) = ~1
   83.43        | is_all _ = 0;
   83.44    in
    84.1 --- a/src/HOL/Tools/simpdata.ML	Fri Mar 21 15:36:00 2014 +0000
    84.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Mar 21 20:39:54 2014 +0100
    84.3 @@ -43,7 +43,7 @@
    84.4  
    84.5  fun mk_eq th = case concl_of th
    84.6    (*expects Trueprop if not == *)
    84.7 -  of Const (@{const_name "=="},_) $ _ $ _ => th
    84.8 +  of Const (@{const_name Pure.eq},_) $ _ $ _ => th
    84.9     | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
   84.10     | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
   84.11     | _ => th RS @{thm Eq_TrueI}
    85.1 --- a/src/HOL/Typerep.thy	Fri Mar 21 15:36:00 2014 +0000
    85.2 +++ b/src/HOL/Typerep.thy	Fri Mar 21 20:39:54 2014 +0100
    85.3 @@ -24,7 +24,7 @@
    85.4    let
    85.5      fun typerep_tr (*"_TYPEREP"*) [ty] =
    85.6            Syntax.const @{const_syntax typerep} $
    85.7 -            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
    85.8 +            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax Pure.type} $
    85.9                (Syntax.const @{type_syntax itself} $ ty))
   85.10        | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
   85.11    in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
   85.12 @@ -34,7 +34,7 @@
   85.13    let
   85.14      fun typerep_tr' ctxt (*"typerep"*)
   85.15              (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
   85.16 -            (Const (@{const_syntax TYPE}, _) :: ts) =
   85.17 +            (Const (@{const_syntax Pure.type}, _) :: ts) =
   85.18            Term.list_comb
   85.19              (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
   85.20        | typerep_tr' _ T ts = raise Match;
    86.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Mar 21 15:36:00 2014 +0000
    86.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Mar 21 20:39:54 2014 +0100
    86.3 @@ -325,7 +325,7 @@
    86.4  refute [expect = genuine]
    86.5  oops
    86.6  
    86.7 -lemma "(x == all) \<Longrightarrow> False"
    86.8 +lemma "(x == Pure.all) \<Longrightarrow> False"
    86.9  refute [expect = genuine]
   86.10  oops
   86.11  
    87.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 15:36:00 2014 +0000
    87.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 20:39:54 2014 +0100
    87.3 @@ -100,7 +100,7 @@
    87.4        | fm t = replace t
    87.5      (*entry point, and abstraction of a meta-formula*)
    87.6      fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
    87.7 -      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    87.8 +      | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q)  = c $ (mt p) $ (mt q)
    87.9        | mt t = fm t  (*it might be a formula*)
   87.10    in (Logic.list_all (params, mt body), !pairs) end;
   87.11  
    88.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Mar 21 15:36:00 2014 +0000
    88.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 21 20:39:54 2014 +0100
    88.3 @@ -232,7 +232,7 @@
    88.4        | fm pos t = var(t,[]);
    88.5        (*entry point, and translation of a meta-formula*)
    88.6        fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
    88.7 -        | mt pos ((c as Const("==>", _)) $ p $ q) =
    88.8 +        | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) =
    88.9              Buildin("=>", [mt (not pos) p, mt pos q])
   88.10          | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   88.11  
    89.1 --- a/src/Provers/blast.ML	Fri Mar 21 15:36:00 2014 +0000
    89.2 +++ b/src/Provers/blast.ML	Fri Mar 21 20:39:54 2014 +0100
    89.3 @@ -419,11 +419,12 @@
    89.4  
    89.5  
    89.6  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    89.7 -fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
    89.8 +fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) =
    89.9 +      strip_Trueprop A :: strip_imp_prems B
   89.10    | strip_imp_prems _ = [];
   89.11  
   89.12  (* A1==>...An==>B  goes to B, where B is not an implication *)
   89.13 -fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
   89.14 +fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B
   89.15    | strip_imp_concl A = strip_Trueprop A;
   89.16  
   89.17  
   89.18 @@ -443,7 +444,7 @@
   89.19            else P :: delete_concl Ps
   89.20        | _ => P :: delete_concl Ps);
   89.21  
   89.22 -fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
   89.23 +fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) =
   89.24          skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
   89.25    | skoPrem _ _ P = P;
   89.26  
   89.27 @@ -1177,7 +1178,7 @@
   89.28  (*Make a list of all the parameters in a subgoal, even if nested*)
   89.29  local open Term
   89.30  in
   89.31 -fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
   89.32 +fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t
   89.33    | discard_foralls t = t;
   89.34  end;
   89.35  
    90.1 --- a/src/Provers/hypsubst.ML	Fri Mar 21 15:36:00 2014 +0000
    90.2 +++ b/src/Provers/hypsubst.ML	Fri Mar 21 20:39:54 2014 +0100
    90.3 @@ -104,8 +104,8 @@
    90.4  (*Locates a substitutable variable on the left (resp. right) of an equality
    90.5     assumption.  Returns the number of intervening assumptions. *)
    90.6  fun eq_var bnd novars =
    90.7 -  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    90.8 -        | eq_var_aux k (Const("==>",_) $ A $ B) =
    90.9 +  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
   90.10 +        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
   90.11                ((k, inspect_pair bnd novars
   90.12                      (Data.dest_eq (Data.dest_Trueprop A)))
   90.13                 handle TERM _ => eq_var_aux (k+1) B
    91.1 --- a/src/Provers/splitter.ML	Fri Mar 21 15:36:00 2014 +0000
    91.2 +++ b/src/Provers/splitter.ML	Fri Mar 21 20:39:54 2014 +0100
    91.3 @@ -57,7 +57,7 @@
    91.4  fun split_format_err () = error "Wrong format for split rule";
    91.5  
    91.6  fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
    91.7 -     Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
    91.8 +     Const(@{const_name Pure.eq}, _) $ (Var _ $ t) $ c => (case strip_comb t of
    91.9         (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
   91.10       | _ => split_format_err ())
   91.11     | _ => split_format_err ();
   91.12 @@ -393,9 +393,9 @@
   91.13        fun tac (t,i) =
   91.14            let val n = find_index (exists_Const (member (op =) cname_list o #1))
   91.15                                   (Logic.strip_assums_hyp t);
   91.16 -              fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _)
   91.17 +              fun first_prem_is_disj (Const (@{const_name Pure.imp}, _) $ (Const (c, _)
   91.18                      $ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or
   91.19 -              |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
   91.20 +              |   first_prem_is_disj (Const(@{const_name Pure.all},_)$Abs(_,_,t)) =
   91.21                                          first_prem_is_disj t
   91.22                |   first_prem_is_disj _ = false;
   91.23        (* does not work properly if the split variable is bound by a quantifier *)
    92.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 21 15:36:00 2014 +0000
    92.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 21 20:39:54 2014 +0100
    92.3 @@ -108,7 +108,7 @@
    92.4  
    92.5  val _ =
    92.6    Outer_Syntax.command @{command_spec "consts"} "declare constants"
    92.7 -    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
    92.8 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
    92.9  
   92.10  val mode_spec =
   92.11    (@{keyword "output"} >> K ("", false)) ||
   92.12 @@ -119,11 +119,13 @@
   92.13  
   92.14  val _ =
   92.15    Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
   92.16 -    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   92.17 +    (opt_mode -- Scan.repeat1 Parse.const_decl
   92.18 +      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   92.19  
   92.20  val _ =
   92.21    Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
   92.22 -    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   92.23 +    (opt_mode -- Scan.repeat1 Parse.const_decl
   92.24 +      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   92.25  
   92.26  
   92.27  (* translations *)
    93.1 --- a/src/Pure/Isar/object_logic.ML	Fri Mar 21 15:36:00 2014 +0000
    93.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Mar 21 20:39:54 2014 +0100
    93.3 @@ -97,8 +97,8 @@
    93.4  
    93.5  in
    93.6  
    93.7 -val add_judgment = gen_add_judgment Sign.add_consts_i;
    93.8 -val add_judgment_cmd = gen_add_judgment Sign.add_consts;
    93.9 +val add_judgment = gen_add_judgment Sign.add_consts;
   93.10 +val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd;
   93.11  
   93.12  end;
   93.13  
    94.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 21 15:36:00 2014 +0000
    94.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 21 20:39:54 2014 +0100
    94.3 @@ -37,7 +37,7 @@
    94.4  val add_syntax =
    94.5    Sign.root_path
    94.6    #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    94.7 -  #> Sign.add_consts_i
    94.8 +  #> Sign.add_consts
    94.9        [(Binding.name "typeof", typ "'b => Type", NoSyn),
   94.10         (Binding.name "Type", typ "'a itself => Type", NoSyn),
   94.11         (Binding.name "Null", typ "Null", NoSyn),
   94.12 @@ -791,7 +791,7 @@
   94.13               val fu = Type.legacy_freeze u;
   94.14               val (def_thms, thy') = if t = nullt then ([], thy) else
   94.15                 thy
   94.16 -               |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
   94.17 +               |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
   94.18                 |> Global_Theory.add_defs false
   94.19                    [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
   94.20                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    95.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 15:36:00 2014 +0000
    95.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 20:39:54 2014 +0100
    95.3 @@ -48,14 +48,14 @@
    95.4              SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    95.5  
    95.6        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    95.7 -        (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    95.8 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
    95.9            _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
   95.10          ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
   95.11          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
   95.12  
   95.13        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
   95.14          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   95.15 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
   95.16 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
   95.17               _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
   95.18          ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
   95.19          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
   95.20 @@ -63,7 +63,7 @@
   95.21  
   95.22        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   95.23          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.24 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
   95.25 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
   95.26               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
   95.27          let
   95.28            val _ $ A $ C = Envir.beta_norm X;
   95.29 @@ -78,7 +78,7 @@
   95.30        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   95.31          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   95.32            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.33 -            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
   95.34 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
   95.35                 (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
   95.36          let
   95.37            val _ $ A $ C = Envir.beta_norm Y;
   95.38 @@ -91,7 +91,7 @@
   95.39          end
   95.40  
   95.41        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   95.42 -        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   95.43 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
   95.44            (PAxm ("Pure.reflexive", _, _) % _) %%
   95.45              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
   95.46          let
   95.47 @@ -104,7 +104,7 @@
   95.48  
   95.49        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   95.50          (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
   95.51 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   95.52 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
   95.53              (PAxm ("Pure.reflexive", _, _) % _) %%
   95.54                (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
   95.55          let
   95.56 @@ -140,7 +140,7 @@
   95.57        | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   95.58          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   95.59            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.60 -            (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   95.61 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   95.62                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   95.63            SOME (equal_elim_axm %> C %> D %% prf2 %%
   95.64              (equal_elim_axm %> A %> C %% prf3 %%
   95.65 @@ -150,7 +150,7 @@
   95.66          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   95.67            (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   95.68              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.69 -              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   95.70 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   95.71                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   95.72            SOME (equal_elim_axm %> A %> B %% prf1 %%
   95.73              (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
   95.74 @@ -160,7 +160,7 @@
   95.75          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   95.76            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   95.77              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.78 -              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   95.79 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   95.80                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   95.81            SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
   95.82              (equal_elim_axm %> B %> D %% prf3 %%
   95.83 @@ -171,14 +171,14 @@
   95.84            (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   95.85              (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   95.86                (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   95.87 -                (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   95.88 +                (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   95.89                    (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   95.90            SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
   95.91              (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
   95.92                (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   95.93  
   95.94        | rew' ((prf as PAxm ("Pure.combination", _, _) %
   95.95 -        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   95.96 +        SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
   95.97            (PAxm ("Pure.reflexive", _, _) % _)) =
   95.98          let val (U, V) = (case T of
   95.99            Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
  95.100 @@ -307,9 +307,9 @@
  95.101      val Hs' = Logic.strip_assums_hyp Q;
  95.102      val k = length Hs;
  95.103      val l = length params;
  95.104 -    fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
  95.105 +    fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
  95.106            mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
  95.107 -      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
  95.108 +      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
  95.109            mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
  95.110        | mk_prf _ _ _ _ _ prf = prf
  95.111    in
  95.112 @@ -324,9 +324,9 @@
  95.113      val Hs' = Logic.strip_assums_hyp Q;
  95.114      val k = length Hs;
  95.115      val l = length params;
  95.116 -    fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
  95.117 +    fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
  95.118            Abst (s, SOME T, mk_prf P prf)
  95.119 -      | mk_prf (Const ("==>", _) $ P $ Q) prf =
  95.120 +      | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
  95.121            AbsP ("H", SOME P, mk_prf Q prf)
  95.122        | mk_prf _ prf = prf
  95.123    in
    96.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 15:36:00 2014 +0000
    96.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 20:39:54 2014 +0100
    96.3 @@ -35,7 +35,7 @@
    96.4  fun add_proof_atom_consts names thy =
    96.5    thy
    96.6    |> Sign.root_path
    96.7 -  |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    96.8 +  |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    96.9  
   96.10  (** constants for application and abstraction **)
   96.11  
   96.12 @@ -54,7 +54,7 @@
   96.13         ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
   96.14         ((Binding.name "MinProof", proofT), Delimfix "?")]
   96.15    |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
   96.16 -  |> Sign.add_syntax_i
   96.17 +  |> Sign.add_syntax Syntax.mode_default
   96.18        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
   96.19         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
   96.20         ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
   96.21 @@ -62,7 +62,7 @@
   96.22         ("", paramT --> paramT, Delimfix "'(_')"),
   96.23         ("", idtT --> paramsT, Delimfix "_"),
   96.24         ("", paramT --> paramsT, Delimfix "_")]
   96.25 -  |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   96.26 +  |> Sign.add_syntax (Symbol.xsymbolsN, true)
   96.27        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
   96.28         (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
   96.29         (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
   96.30 @@ -127,16 +127,16 @@
   96.31              Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
   96.32        | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   96.33            AbsP (s, case t of
   96.34 -                Const ("dummy_pattern", _) => NONE
   96.35 -              | _ $ Const ("dummy_pattern", _) => NONE
   96.36 +                Const ("Pure.dummy_pattern", _) => NONE
   96.37 +              | _ $ Const ("Pure.dummy_pattern", _) => NONE
   96.38                | _ => SOME (mk_term t),
   96.39              Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
   96.40        | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   96.41            prf_of [] prf1 %% prf_of [] prf2
   96.42 -      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   96.43 +      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
   96.44            prf_of (T::Ts) prf
   96.45        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   96.46 -          (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   96.47 +          (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   96.48        | prf_of _ t = error ("Not a proof term:\n" ^
   96.49            Syntax.string_of_term_global thy t)
   96.50  
    97.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Mar 21 15:36:00 2014 +0000
    97.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Mar 21 20:39:54 2014 +0100
    97.3 @@ -155,7 +155,7 @@
    97.4                | SOME T => (T, env));
    97.5              val (t, prf, cnstrts, env'', vTs') =
    97.6                mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
    97.7 -          in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
    97.8 +          in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
    97.9              cnstrts, env'', vTs')
   97.10            end
   97.11        | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
   97.12 @@ -173,7 +173,7 @@
   97.13        | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) =
   97.14            let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2
   97.15            in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of
   97.16 -              (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
   97.17 +              (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
   97.18                  add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts)
   97.19                    env'' vTs'' (u, u')
   97.20              | (t, prf1, cnstrts', env'', vTs'') =>
   97.21 @@ -185,7 +185,7 @@
   97.22        | mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
   97.23            let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
   97.24            in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
   97.25 -             (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   97.26 +             (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   97.27                   prf, cnstrts, env2, vTs2) =>
   97.28                 let val env3 = unifyT thy env2 T U
   97.29                 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
   97.30 @@ -194,12 +194,12 @@
   97.31                 let val (v, env3) = mk_var env2 Ts (U --> propT);
   97.32                 in
   97.33                   add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2
   97.34 -                   (u, Const ("all", (U --> propT) --> propT) $ v)
   97.35 +                   (u, Const ("Pure.all", (U --> propT) --> propT) $ v)
   97.36                 end)
   97.37            end
   97.38        | mk_cnstrts env Ts Hs vTs (cprf % NONE) =
   97.39            (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of
   97.40 -             (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   97.41 +             (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
   97.42                   prf, cnstrts, env', vTs') =>
   97.43                 let val (t, env'') = mk_var env' Ts T
   97.44                 in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs')
   97.45 @@ -211,7 +211,7 @@
   97.46                   val (t, env3) = mk_var env2 Ts T
   97.47                 in
   97.48                   add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
   97.49 -                   (u, Const ("all", (T --> propT) --> propT) $ v)
   97.50 +                   (u, Const ("Pure.all", (T --> propT) --> propT) $ v)
   97.51                 end)
   97.52        | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
   97.53            mk_cnstrts_atom env vTs prop opTs prf
   97.54 @@ -309,10 +309,10 @@
   97.55    | prop_of0 Hs (AbsP (s, SOME t, prf)) =
   97.56        Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
   97.57    | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
   97.58 -      Const ("all", _) $ f => f $ t
   97.59 +      Const ("Pure.all", _) $ f => f $ t
   97.60      | _ => error "prop_of: all expected")
   97.61    | prop_of0 Hs (prf1 %% prf2) = (case head_norm (prop_of0 Hs prf1) of
   97.62 -      Const ("==>", _) $ P $ Q => Q
   97.63 +      Const ("Pure.imp", _) $ P $ Q => Q
   97.64      | _ => error "prop_of: ==> expected")
   97.65    | prop_of0 Hs (Hyp t) = t
   97.66    | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
    98.1 --- a/src/Pure/Syntax/simple_syntax.ML	Fri Mar 21 15:36:00 2014 +0000
    98.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Fri Mar 21 20:39:54 2014 +0100
    98.3 @@ -107,12 +107,12 @@
    98.4   (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
    98.5    term2 env T) x
    98.6  and term2 env T x =
    98.7 - (equal env "==" ||
    98.8 + (equal env ||
    98.9    term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   98.10    term3 env T) x
   98.11 -and equal env eq x =
   98.12 - (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
   98.13 -   Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   98.14 +and equal env x =
   98.15 + (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) =>
   98.16 +   Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   98.17  and term3 env T x =
   98.18   (idt >> Free ||
   98.19    var -- constraint >> Var ||
    99.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 15:36:00 2014 +0000
    99.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 20:39:54 2014 +0100
    99.3 @@ -177,7 +177,7 @@
    99.4            in [Ast.Constant (Lexicon.mark_type c)] end
    99.5        | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
    99.6        | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
    99.7 -      | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
    99.8 +      | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
    99.9            [ast_of_dummy a tok]
   99.10        | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
   99.11            [ast_of_dummy a tok]
   99.12 @@ -568,7 +568,7 @@
   99.13        | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
   99.14        | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
   99.15        | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
   99.16 -      | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
   99.17 +      | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) =
   99.18            if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
   99.19            else mark Ts t1 $ mark Ts t2
   99.20        | mark Ts (t as t1 $ t2) =
   99.21 @@ -834,7 +834,7 @@
   99.22      ("_context_xconst", const_ast_tr false)] #>
   99.23    Sign.typed_print_translation
   99.24     [("_type_prop", type_prop_tr'),
   99.25 -    ("\\<^const>TYPE", type_tr'),
   99.26 +    ("\\<^const>Pure.type", type_tr'),
   99.27      ("_type_constraint_", type_constraint_tr')]);
   99.28  
   99.29  
   100.1 --- a/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 15:36:00 2014 +0000
   100.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 20:39:54 2014 +0100
   100.3 @@ -152,7 +152,7 @@
   100.4  
   100.5  fun mk_type ty =
   100.6    Syntax.const "_constrain" $
   100.7 -    Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);
   100.8 +    Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
   100.9  
  100.10  fun ofclass_tr [ty, cls] = cls $ mk_type ty
  100.11    | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
  100.12 @@ -174,7 +174,7 @@
  100.13          (case Ast.unfold_ast_p "_asms" asms of
  100.14            (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
  100.15          | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
  100.16 -      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
  100.17 +      in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
  100.18    | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
  100.19  
  100.20  
  100.21 @@ -382,7 +382,8 @@
  100.22  fun impl_ast_tr' asts =
  100.23    if no_brackets () then raise Match
  100.24    else
  100.25 -    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
  100.26 +    (case Ast.unfold_ast_p "\\<^const>Pure.imp"
  100.27 +        (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
  100.28        (prems as _ :: _ :: _, concl) =>
  100.29          let
  100.30            val (asms, asm) = split_last prems;
  100.31 @@ -498,7 +499,7 @@
  100.32    ("_abs", fn _ => abs_ast_tr'),
  100.33    ("_idts", fn _ => idtyp_ast_tr' "_idts"),
  100.34    ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
  100.35 -  ("\\<^const>==>", fn _ => impl_ast_tr'),
  100.36 +  ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
  100.37    ("_index", fn _ => index_ast_tr')];
  100.38  
  100.39  end;
   101.1 --- a/src/Pure/conv.ML	Fri Mar 21 15:36:00 2014 +0000
   101.2 +++ b/src/Pure/conv.ML	Fri Mar 21 20:39:54 2014 +0100
   101.3 @@ -140,17 +140,17 @@
   101.4  
   101.5  fun forall_conv cv ctxt ct =
   101.6    (case Thm.term_of ct of
   101.7 -    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   101.8 +    Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   101.9    | _ => raise CTERM ("forall_conv", [ct]));
  101.10  
  101.11  fun implies_conv cv1 cv2 ct =
  101.12    (case Thm.term_of ct of
  101.13 -    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
  101.14 +    Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
  101.15    | _ => raise CTERM ("implies_conv", [ct]));
  101.16  
  101.17  fun implies_concl_conv cv ct =
  101.18    (case Thm.term_of ct of
  101.19 -    Const ("==>", _) $ _ $ _ => arg_conv cv ct
  101.20 +    Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
  101.21    | _ => raise CTERM ("implies_concl_conv", [ct]));
  101.22  
  101.23  
   102.1 --- a/src/Pure/drule.ML	Fri Mar 21 15:36:00 2014 +0000
   102.2 +++ b/src/Pure/drule.ML	Fri Mar 21 20:39:54 2014 +0100
   102.3 @@ -126,7 +126,7 @@
   102.4  (* A1==>...An==>B  goes to B, where B is not an implication *)
   102.5  fun strip_imp_concl ct =
   102.6    (case Thm.term_of ct of
   102.7 -    Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
   102.8 +    Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
   102.9    | _ => ct);
  102.10  
  102.11  (*The premises of a theorem, as a cterm list*)
  102.12 @@ -706,7 +706,7 @@
  102.13  val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
  102.14  
  102.15  fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
  102.16 -  | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
  102.17 +  | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
  102.18    | is_norm_hhf (Abs _ $ _) = false
  102.19    | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u
  102.20    | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
   103.1 --- a/src/Pure/goal.ML	Fri Mar 21 15:36:00 2014 +0000
   103.2 +++ b/src/Pure/goal.ML	Fri Mar 21 20:39:54 2014 +0100
   103.3 @@ -327,8 +327,8 @@
   103.4  
   103.5  (* non-atomic goal assumptions *)
   103.6  
   103.7 -fun non_atomic (Const ("==>", _) $ _ $ _) = true
   103.8 -  | non_atomic (Const ("all", _) $ _) = true
   103.9 +fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true
  103.10 +  | non_atomic (Const ("Pure.all", _) $ _) = true
  103.11    | non_atomic _ = false;
  103.12  
  103.13  fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
   104.1 --- a/src/Pure/logic.ML	Fri Mar 21 15:36:00 2014 +0000
   104.2 +++ b/src/Pure/logic.ML	Fri Mar 21 20:39:54 2014 +0100
   104.3 @@ -93,14 +93,14 @@
   104.4  
   104.5  (** all **)
   104.6  
   104.7 -fun all_const T = Const ("all", (T --> propT) --> propT);
   104.8 +fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
   104.9  
  104.10  fun all v t = all_const (Term.fastype_of v) $ lambda v t;
  104.11  
  104.12 -fun is_all (Const ("all", _) $ Abs _) = true
  104.13 +fun is_all (Const ("Pure.all", _) $ Abs _) = true
  104.14    | is_all _ = false;
  104.15  
  104.16 -fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
  104.17 +fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
  104.18        let val (x, b) = Term.dest_abs abs  (*potentially slow*)
  104.19        in ((x, T), b) end
  104.20    | dest_all t = raise TERM ("dest_all", [t]);
  104.21 @@ -113,19 +113,19 @@
  104.22  
  104.23  fun mk_equals (t, u) =
  104.24    let val T = Term.fastype_of t
  104.25 -  in Const ("==", T --> T --> propT) $ t $ u end;
  104.26 +  in Const ("Pure.eq", T --> T --> propT) $ t $ u end;
  104.27  
  104.28 -fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
  104.29 +fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
  104.30    | dest_equals t = raise TERM ("dest_equals", [t]);
  104.31  
  104.32  
  104.33  (** implies **)
  104.34  
  104.35 -val implies = Const ("==>", propT --> propT --> propT);
  104.36 +val implies = Const ("Pure.imp", propT --> propT --> propT);
  104.37  
  104.38  fun mk_implies (A, B) = implies $ A $ B;
  104.39  
  104.40 -fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
  104.41 +fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B)
  104.42    | dest_implies A = raise TERM ("dest_implies", [A]);
  104.43  
  104.44  
  104.45 @@ -136,28 +136,28 @@
  104.46    | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
  104.47  
  104.48  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
  104.49 -fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
  104.50 +fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
  104.51    | strip_imp_prems _ = [];
  104.52  
  104.53  (* A1==>...An==>B  goes to B, where B is not an implication *)
  104.54 -fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
  104.55 +fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
  104.56    | strip_imp_concl A = A : term;
  104.57  
  104.58  (*Strip and return premises: (i, [], A1==>...Ai==>B)
  104.59      goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
  104.60    if  i<0 or else i too big then raises  TERM*)
  104.61  fun strip_prems (0, As, B) = (As, B)
  104.62 -  | strip_prems (i, As, Const("==>", _) $ A $ B) =
  104.63 +  | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) =
  104.64          strip_prems (i-1, A::As, B)
  104.65    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
  104.66  
  104.67  (*Count premises -- quicker than (length o strip_prems) *)
  104.68 -fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
  104.69 +fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
  104.70    | count_prems _ = 0;
  104.71  
  104.72  (*Select Ai from A1 ==>...Ai==>B*)
  104.73 -fun nth_prem (1, Const ("==>", _) $ A $ _) = A
  104.74 -  | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
  104.75 +fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
  104.76 +  | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
  104.77    | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
  104.78  
  104.79  (*strip a proof state (Horn clause):
  104.80 @@ -208,9 +208,9 @@
  104.81  
  104.82  (** types as terms **)
  104.83  
  104.84 -fun mk_type ty = Const ("TYPE", Term.itselfT ty);
  104.85 +fun mk_type ty = Const ("Pure.type", Term.itselfT ty);
  104.86  
  104.87 -fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
  104.88 +fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty
  104.89    | dest_type t = raise TERM ("dest_type", [t]);
  104.90  
  104.91  fun type_map f = dest_type o f o mk_type;
  104.92 @@ -323,10 +323,10 @@
  104.93  
  104.94  (** protected propositions and embedded terms **)
  104.95  
  104.96 -val protectC = Const ("prop", propT --> propT);
  104.97 +val protectC = Const ("Pure.prop", propT --> propT);
  104.98  fun protect t = protectC $ t;
  104.99  
 104.100 -fun unprotect (Const ("prop", _) $ t) = t
 104.101 +fun unprotect (Const ("Pure.prop", _) $ t) = t
 104.102    | unprotect t = raise TERM ("unprotect", [t]);
 104.103  
 104.104  
 104.105 @@ -395,46 +395,46 @@
 104.106  
 104.107  fun lift_abs inc =
 104.108    let
 104.109 -    fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
 104.110 -      | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
 104.111 +    fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
 104.112 +      | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
 104.113        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
 104.114    in lift [] end;
 104.115  
 104.116  fun lift_all inc =
 104.117    let
 104.118 -    fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
 104.119 -      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
 104.120 +    fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
 104.121 +      | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
 104.122        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
 104.123    in lift [] end;
 104.124  
 104.125  (*Strips assumptions in goal, yielding list of hypotheses.   *)
 104.126  fun strip_assums_hyp B =
 104.127    let
 104.128 -    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
 104.129 -      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
 104.130 +    fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B
 104.131 +      | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) =
 104.132            strip (map (incr_boundvars 1) Hs) t
 104.133        | strip Hs B = rev Hs
 104.134    in strip [] B end;
 104.135  
 104.136  (*Strips assumptions in goal, yielding conclusion.   *)
 104.137 -fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
 104.138 -  | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
 104.139 +fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
 104.140 +  | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t
 104.141    | strip_assums_concl B = B;
 104.142  
 104.143  (*Make a list of all the parameters in a subgoal, even if nested*)
 104.144 -fun strip_params (Const("==>", _) $ H $ B) = strip_params B
 104.145 -  | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
 104.146 +fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
 104.147 +  | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
 104.148    | strip_params B = [];
 104.149  
 104.150  (*test for nested meta connectives in prems*)
 104.151  val has_meta_prems =
 104.152    let
 104.153 -    fun is_meta (Const ("==", _) $ _ $ _) = true
 104.154 -      | is_meta (Const ("==>", _) $ _ $ _) = true
 104.155 -      | is_meta (Const ("all", _) $ _) = true
 104.156 +    fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true
 104.157 +      | is_meta (Const ("Pure.imp", _) $ _ $ _) = true
 104.158 +      | is_meta (Const ("Pure.all", _) $ _) = true
 104.159        | is_meta _ = false;
 104.160 -    fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
 104.161 -      | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
 104.162 +    fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B
 104.163 +      | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B
 104.164        | ex_meta _ = false;
 104.165    in ex_meta end;
 104.166  
 104.167 @@ -444,10 +444,10 @@
 104.168  fun remove_params j n A =
 104.169      if j=0 andalso n<=0 then A  (*nothing left to do...*)
 104.170      else case A of
 104.171 -        Const("==>", _) $ H $ B =>
 104.172 +        Const("Pure.imp", _) $ H $ B =>
 104.173            if n=1 then                           (remove_params j (n-1) B)
 104.174            else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
 104.175 -      | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
 104.176 +      | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t
 104.177        | _ => if n>0 then raise TERM("remove_params", [A])
 104.178               else A;
 104.179  
 104.180 @@ -460,9 +460,9 @@
 104.181      in list_all (vars, remove_params (length vars) n A) end;
 104.182  
 104.183  (*Makes parameters in a goal have the names supplied by the list cs.*)
 104.184 -fun list_rename_params cs (Const ("==>", _) $ A $ B) =
 104.185 +fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) =
 104.186        implies $ A $ list_rename_params cs B
 104.187 -  | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
 104.188 +  | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) =
 104.189        a $ Abs (c, T, list_rename_params cs t)
 104.190    | list_rename_params cs B = B;
 104.191  
 104.192 @@ -480,12 +480,12 @@
 104.193        Unless nasms<0, it can terminate the recursion early; that allows
 104.194    erule to work on assumptions of the form P==>Q.*)
 104.195  fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
 104.196 -  | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
 104.197 +  | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
 104.198        strip_assums_imp (nasms-1, H::Hs, B)
 104.199    | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
 104.200  
 104.201  (*Strips OUTER parameters only.*)
 104.202 -fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
 104.203 +fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) =
 104.204        strip_assums_all ((a,T)::params, t)
 104.205    | strip_assums_all (params, B) = (params, B);
 104.206  
   105.1 --- a/src/Pure/more_thm.ML	Fri Mar 21 15:36:00 2014 +0000
   105.2 +++ b/src/Pure/more_thm.ML	Fri Mar 21 20:39:54 2014 +0100
   105.3 @@ -127,7 +127,7 @@
   105.4    let
   105.5      val cert = Thm.cterm_of (Thm.theory_of_cterm t);
   105.6      val T = #T (Thm.rep_cterm t);
   105.7 -  in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
   105.8 +  in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
   105.9  
  105.10  fun all t A = all_name ("", t) A;
  105.11  
  105.12 @@ -136,22 +136,22 @@
  105.13  
  105.14  fun dest_implies ct =
  105.15    (case Thm.term_of ct of
  105.16 -    Const ("==>", _) $ _ $ _ => dest_binop ct
  105.17 +    Const ("Pure.imp", _) $ _ $ _ => dest_binop ct
  105.18    | _ => raise TERM ("dest_implies", [Thm.term_of ct]));
  105.19  
  105.20  fun dest_equals ct =
  105.21    (case Thm.term_of ct of
  105.22 -    Const ("==", _) $ _ $ _ => dest_binop ct
  105.23 +    Const ("Pure.eq", _) $ _ $ _ => dest_binop ct
  105.24    | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
  105.25  
  105.26  fun dest_equals_lhs ct =
  105.27    (case Thm.term_of ct of
  105.28 -    Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
  105.29 +    Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct
  105.30    | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
  105.31  
  105.32  fun dest_equals_rhs ct =
  105.33    (case Thm.term_of ct of
  105.34 -    Const ("==", _) $ _ $ _ => Thm.dest_arg ct
  105.35 +    Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct
  105.36    | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
  105.37  
  105.38  val lhs_of = dest_equals_lhs o Thm.cprop_of;
  105.39 @@ -337,7 +337,7 @@
  105.40  
  105.41  fun forall_elim_var i th =
  105.42    forall_elim_vars_aux
  105.43 -    (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
  105.44 +    (fn Const ("Pure.all", _) $ Abs (a, T, _) => [(a, T)]
  105.45        | _ => raise THM ("forall_elim_vars", i, [th])) i th;
  105.46  
  105.47  end;
   106.1 --- a/src/Pure/primitive_defs.ML	Fri Mar 21 15:36:00 2014 +0000
   106.2 +++ b/src/Pure/primitive_defs.ML	Fri Mar 21 20:39:54 2014 +0100
   106.3 @@ -37,7 +37,7 @@
   106.4  
   106.5      fun check_arg (Bound _) = true
   106.6        | check_arg (Free (x, _)) = not (is_fixed x)
   106.7 -      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   106.8 +      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
   106.9        | check_arg _ = false;
  106.10      fun close_arg (Bound _) t = t
  106.11        | close_arg x t = Logic.all x t;
   107.1 --- a/src/Pure/proofterm.ML	Fri Mar 21 15:36:00 2014 +0000
   107.2 +++ b/src/Pure/proofterm.ML	Fri Mar 21 20:39:54 2014 +0100
   107.3 @@ -865,9 +865,9 @@
   107.4      fun mk_app b (i, j, prf) =
   107.5            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
   107.6  
   107.7 -    fun lift Us bs i j (Const ("==>", _) $ A $ B) =
   107.8 +    fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
   107.9              AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
  107.10 -      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
  107.11 +      | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
  107.12              Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
  107.13        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
  107.14              map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
  107.15 @@ -886,9 +886,9 @@
  107.16  fun mk_asm_prf t i m =
  107.17    let
  107.18      fun imp_prf _ i 0 = PBound i
  107.19 -      | imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
  107.20 +      | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
  107.21        | imp_prf _ i _ = PBound i;
  107.22 -    fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
  107.23 +    fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
  107.24        | all_prf t = imp_prf t (~i) m
  107.25    in all_prf t end;
  107.26  
  107.27 @@ -899,9 +899,9 @@
  107.28  
  107.29  (***** Composition of object rule with proof state *****)
  107.30  
  107.31 -fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) =
  107.32 +fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
  107.33        AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
  107.34 -  | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) =
  107.35 +  | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) =
  107.36        Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
  107.37    | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
  107.38        map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
  107.39 @@ -1091,9 +1091,9 @@
  107.40        if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
  107.41    else vs;
  107.42  
  107.43 -fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
  107.44 +fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) =
  107.45        add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
  107.46 -  | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) =
  107.47 +  | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) =
  107.48        add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
  107.49    | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
  107.50    | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
  107.51 @@ -1105,8 +1105,8 @@
  107.52    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
  107.53    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
  107.54  
  107.55 -fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
  107.56 -  | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
  107.57 +fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
  107.58 +  | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
  107.59    | prop_vars t = (case strip_comb t of
  107.60        (Var (ixn, _), _) => [ixn] | _ => []);
  107.61  
  107.62 @@ -1196,7 +1196,7 @@
  107.63                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
  107.64                  | (_, x) => (false, x)) insts
  107.65            in ([], false, insts' @ map (pair false) ts'', prf) end
  107.66 -    and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
  107.67 +    and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) =
  107.68            union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
  107.69        | needed (Var (ixn, _)) (_::_) _ = [ixn]
  107.70        | needed _ _ _ = [];
   108.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 15:36:00 2014 +0000
   108.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 20:39:54 2014 +0100
   108.3 @@ -49,8 +49,8 @@
   108.4  
   108.5  val old_appl_syntax_setup =
   108.6    Old_Appl_Syntax.put true #>
   108.7 -  Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
   108.8 -  Sign.add_syntax_i appl_syntax;
   108.9 +  Sign.del_syntax Syntax.mode_default applC_syntax #>
  108.10 +  Sign.add_syntax Syntax.mode_default appl_syntax;
  108.11  
  108.12  
  108.13  (* main content *)
  108.14 @@ -75,8 +75,8 @@
  108.15          "tvar_position", "id_position", "longid_position", "var_position",
  108.16          "str_position", "string_position", "cartouche_position", "type_name",
  108.17          "class_name"]))
  108.18 -  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
  108.19 -  #> Sign.add_syntax_i
  108.20 +  #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
  108.21 +  #> Sign.add_syntax Syntax.mode_default
  108.22     [("",            typ "prop' => prop",               Delimfix "_"),
  108.23      ("",            typ "logic => any",                Delimfix "_"),
  108.24      ("",            typ "prop' => any",                Delimfix "_"),
  108.25 @@ -169,13 +169,13 @@
  108.26      ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
  108.27      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
  108.28      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
  108.29 -    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
  108.30 -    (const "dummy_pattern", typ "aprop",               Delimfix "'_"),
  108.31 +    (const "Pure.imp",  typ "prop => prop => prop",     Delimfix "op ==>"),
  108.32 +    (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
  108.33      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
  108.34      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
  108.35      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
  108.36 -  #> Sign.add_syntax_i applC_syntax
  108.37 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
  108.38 +  #> Sign.add_syntax Syntax.mode_default applC_syntax
  108.39 +  #> Sign.add_syntax (Symbol.xsymbolsN, true)
  108.40     [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
  108.41      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
  108.42      ("_ofsort",           typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
  108.43 @@ -184,42 +184,42 @@
  108.44      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
  108.45      ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
  108.46      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
  108.47 -    (const "==",          typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
  108.48 -    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
  108.49 -    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
  108.50 +    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
  108.51 +    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
  108.52 +    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
  108.53      ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
  108.54      ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
  108.55      ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
  108.56 -  #> Sign.add_modesyntax_i ("", false)
  108.57 -   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
  108.58 -  #> Sign.add_modesyntax_i ("HTML", false)
  108.59 +  #> Sign.add_syntax ("", false)
  108.60 +   [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
  108.61 +  #> Sign.add_syntax ("HTML", false)
  108.62     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
  108.63 -  #> Sign.add_consts_i
  108.64 -   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
  108.65 -    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
  108.66 -    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
  108.67 -    (Binding.name "prop", typ "prop => prop", NoSyn),
  108.68 -    (Binding.name "TYPE", typ "'a itself", NoSyn),
  108.69 -    (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
  108.70 -  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
  108.71 -  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
  108.72 -  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
  108.73 -  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
  108.74 -  #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
  108.75 +  #> Sign.add_consts
  108.76 +   [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
  108.77 +    (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
  108.78 +    (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
  108.79 +    (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
  108.80 +    (qualify (Binding.name "type"), typ "'a itself", NoSyn),
  108.81 +    (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
  108.82 +  #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
  108.83 +  #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
  108.84 +  #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
  108.85 +  #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
  108.86 +  #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
  108.87    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
  108.88    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
  108.89    #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
  108.90 -  #> Sign.add_consts_i
  108.91 +  #> Sign.add_consts
  108.92     [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
  108.93      (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
  108.94      (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
  108.95    #> Sign.local_path
  108.96    #> (Global_Theory.add_defs false o map Thm.no_attributes)
  108.97 -   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
  108.98 +   [(Binding.name "prop_def", prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
  108.99      (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
 108.100      (Binding.name "sort_constraint_def",
 108.101 -      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
 108.102 -      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
 108.103 +      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
 108.104 +      \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
 108.105      (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
 108.106    #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
 108.107    #> fold (fn (a, prop) =>
   109.1 --- a/src/Pure/raw_simplifier.ML	Fri Mar 21 15:36:00 2014 +0000
   109.2 +++ b/src/Pure/raw_simplifier.ML	Fri Mar 21 20:39:54 2014 +0100
   109.3 @@ -599,7 +599,7 @@
   109.4    | is_full_cong_prems [] _ = false
   109.5    | is_full_cong_prems (p :: prems) varpairs =
   109.6        (case Logic.strip_assums_concl p of
   109.7 -        Const ("==", _) $ lhs $ rhs =>
   109.8 +        Const ("Pure.eq", _) $ lhs $ rhs =>
   109.9            let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
  109.10              is_Var x andalso forall is_Bound xs andalso
  109.11              not (has_duplicates (op =) xs) andalso xs = ys andalso
  109.12 @@ -981,7 +981,7 @@
  109.13        let
  109.14          fun is_simple ({thm, ...}: rrule) =
  109.15            (case Thm.prop_of thm of
  109.16 -            Const ("==", _) $ _ $ _ => true
  109.17 +            Const ("Pure.eq", _) $ _ $ _ => true
  109.18            | _ => false);
  109.19          fun sort [] (re1, re2) = re1 @ re2
  109.20            | sort (rr :: rrs) (re1, re2) =
  109.21 @@ -1099,7 +1099,7 @@
  109.22                  end
  109.23              | t $ _ =>
  109.24                (case t of
  109.25 -                Const ("==>", _) $ _  => impc t0 ctxt
  109.26 +                Const ("Pure.imp", _) $ _  => impc t0 ctxt
  109.27                | Abs _ =>
  109.28                    let val thm = Thm.beta_conversion false t0
  109.29                    in
   110.1 --- a/src/Pure/sign.ML	Fri Mar 21 15:36:00 2014 +0000
   110.2 +++ b/src/Pure/sign.ML	Fri Mar 21 20:39:54 2014 +0100
   110.3 @@ -73,18 +73,16 @@
   110.4    val add_nonterminals: Proof.context -> binding list -> theory -> theory
   110.5    val add_nonterminals_global: binding list -> theory -> theory
   110.6    val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
   110.7 -  val add_syntax: (string * string * mixfix) list -> theory -> theory
   110.8 -  val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
   110.9 -  val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
  110.10 -  val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
  110.11 -  val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
  110.12 -  val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
  110.13 +  val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
  110.14 +  val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
  110.15 +  val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
  110.16 +  val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
  110.17    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
  110.18    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
  110.19    val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
  110.20    val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
  110.21 -  val add_consts: (binding * string * mixfix) list -> theory -> theory
  110.22 -  val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
  110.23 +  val add_consts: (binding * typ * mixfix) list -> theory -> theory
  110.24 +  val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
  110.25    val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
  110.26    val revert_abbrev: string -> string -> theory -> theory
  110.27    val add_const_constraint: string * typ option -> theory -> theory
  110.28 @@ -375,12 +373,10 @@
  110.29  
  110.30  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
  110.31  
  110.32 -val add_modesyntax = gen_add_syntax Syntax.read_typ;
  110.33 -val add_modesyntax_i = gen_add_syntax (K I);
  110.34 -val add_syntax = add_modesyntax Syntax.mode_default;
  110.35 -val add_syntax_i = add_modesyntax_i Syntax.mode_default;
  110.36 -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
  110.37 -val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
  110.38 +val add_syntax = gen_add_syntax (K I);
  110.39 +val add_syntax_cmd = gen_add_syntax Syntax.read_typ;
  110.40 +val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I);
  110.41 +val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
  110.42  
  110.43  fun type_notation add mode args =
  110.44    let
  110.45 @@ -417,17 +413,17 @@
  110.46    in
  110.47      thy
  110.48      |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
  110.49 -    |> add_syntax_i (map #2 args)
  110.50 +    |> add_syntax Syntax.mode_default (map #2 args)
  110.51      |> pair (map #3 args)
  110.52    end;
  110.53  
  110.54  in
  110.55  
  110.56  fun add_consts args thy =
  110.57 -  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
  110.58 +  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
  110.59  
  110.60 -fun add_consts_i args thy =
  110.61 -  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
  110.62 +fun add_consts_cmd args thy =
  110.63 +  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
  110.64  
  110.65  fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
  110.66  fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
  110.67 @@ -468,7 +464,7 @@
  110.68    |> map_sign (fn (syn, tsig, consts) =>
  110.69        let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
  110.70        in (syn, tsig', consts) end)
  110.71 -  |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  110.72 +  |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  110.73  
  110.74  fun primitive_classrel arg thy =
  110.75    thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
   111.1 --- a/src/Pure/term.ML	Fri Mar 21 15:36:00 2014 +0000
   111.2 +++ b/src/Pure/term.ML	Fri Mar 21 20:39:54 2014 +0100
   111.3 @@ -579,11 +579,11 @@
   111.4  val propT : typ = Type ("prop",[]);
   111.5  
   111.6  (* maps  !!x1...xn. t   to   t  *)
   111.7 -fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   111.8 +fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t))  =  strip_all_body t
   111.9    | strip_all_body t  =  t;
  111.10  
  111.11  (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
  111.12 -fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
  111.13 +fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t))  =
  111.14                  (a,T) :: strip_all_vars t
  111.15    | strip_all_vars t  =  [] : (string*typ) list;
  111.16  
  111.17 @@ -816,7 +816,7 @@
  111.18  
  111.19  fun close_schematic_term t =
  111.20    let
  111.21 -    val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
  111.22 +    val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t);
  111.23      val extra_terms = map Var (add_vars t []);
  111.24    in fold lambda (extra_terms @ extra_types) t end;
  111.25  
  111.26 @@ -924,18 +924,18 @@
  111.27  
  111.28  (* dummy patterns *)
  111.29  
  111.30 -fun dummy_pattern T = Const ("dummy_pattern", T);
  111.31 +fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
  111.32  val dummy = dummy_pattern dummyT;
  111.33  val dummy_prop = dummy_pattern propT;
  111.34  
  111.35 -fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  111.36 +fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
  111.37    | is_dummy_pattern _ = false;
  111.38  
  111.39  fun no_dummy_patterns tm =
  111.40    if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  111.41    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  111.42  
  111.43 -fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
  111.44 +fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
  111.45        let val [x] = Name.invent used Name.uu 1
  111.46        in (Free (Name.internal x, T), Name.declare x used) end
  111.47    | free_dummy_patterns (Abs (x, T, b)) used =
  111.48 @@ -948,7 +948,7 @@
  111.49        in (t' $ u', used'') end
  111.50    | free_dummy_patterns a used = (a, used);
  111.51  
  111.52 -fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
  111.53 +fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
  111.54        (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
  111.55    | replace_dummy Ts (Abs (x, T, t)) i =
  111.56        let val (t', i') = replace_dummy (T :: Ts) t i
   112.1 --- a/src/Pure/thm.ML	Fri Mar 21 15:36:00 2014 +0000
   112.2 +++ b/src/Pure/thm.ML	Fri Mar 21 20:39:54 2014 +0100
   112.3 @@ -687,7 +687,7 @@
   112.4      fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   112.5    in
   112.6      case prop of
   112.7 -      Const ("==>", _) $ A $ B =>
   112.8 +      Const ("Pure.imp", _) $ A $ B =>
   112.9          if A aconv propA then
  112.10            Thm (deriv_rule2 (curry Proofterm.%%) der derA,
  112.11             {thy = merge_thys2 thAB thA,
  112.12 @@ -741,7 +741,7 @@
  112.13      (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
  112.14      (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
  112.15    (case prop of
  112.16 -    Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
  112.17 +    Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
  112.18        if T <> qary then
  112.19          raise THM ("forall_elim: type mismatch", 0, [th])
  112.20        else
  112.21 @@ -778,7 +778,7 @@
  112.22  *)
  112.23  fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
  112.24    (case prop of
  112.25 -    (eq as Const ("==", _)) $ t $ u =>
  112.26 +    (eq as Const ("Pure.eq", _)) $ t $ u =>
  112.27        Thm (deriv_rule1 Proofterm.symmetric der,
  112.28         {thy = thy,
  112.29          tags = [],
  112.30 @@ -803,7 +803,7 @@
  112.31      fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
  112.32    in
  112.33      case (prop1, prop2) of
  112.34 -      ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
  112.35 +      ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
  112.36          if not (u aconv u') then err "middle term"
  112.37          else
  112.38            Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
  112.39 @@ -911,8 +911,8 @@
  112.40        | _ => raise THM ("combination: not function type", 0, [th1, th2]));
  112.41    in
  112.42      (case (prop1, prop2) of
  112.43 -      (Const ("==", Type ("fun", [fT, _])) $ f $ g,
  112.44 -       Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
  112.45 +      (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
  112.46 +       Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
  112.47          (chktypes fT tT;
  112.48            Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
  112.49             {thy = merge_thys2 th1 th2,
  112.50 @@ -939,7 +939,7 @@
  112.51      fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
  112.52    in
  112.53      (case (prop1, prop2) of
  112.54 -      (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
  112.55 +      (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
  112.56          if A aconv A' andalso B aconv B' then
  112.57            Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
  112.58             {thy = merge_thys2 th1 th2,
  112.59 @@ -967,7 +967,7 @@
  112.60      fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
  112.61    in
  112.62      (case prop1 of
  112.63 -      Const ("==", _) $ A $ B =>
  112.64 +      Const ("Pure.eq", _) $ A $ B =>
  112.65          if prop2 aconv A then
  112.66            Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
  112.67             {thy = merge_thys2 th1 th2,
  112.68 @@ -1472,17 +1472,17 @@
  112.69  (* strip_apply f B A strips off all assumptions/parameters from A
  112.70     introduced by lifting over B, and applies f to remaining part of A*)
  112.71  fun strip_apply f =
  112.72 -  let fun strip (Const ("==>", _) $ _  $ B1)
  112.73 -                (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
  112.74 -        | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
  112.75 -                (      Const ("all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
  112.76 +  let fun strip (Const ("Pure.imp", _) $ _  $ B1)
  112.77 +                (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
  112.78 +        | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
  112.79 +                (      Const ("Pure.all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
  112.80          | strip _ A = f A
  112.81    in strip end;
  112.82  
  112.83 -fun strip_lifted (Const ("==>", _) $ _ $ B1)
  112.84 -                 (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
  112.85 -  | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
  112.86 -                 (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
  112.87 +fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1)
  112.88 +                 (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2
  112.89 +  | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1))
  112.90 +                 (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
  112.91    | strip_lifted _ A = A;
  112.92  
  112.93  (*Use the alist to rename all bound variables and some unknowns in a term
  112.94 @@ -1532,10 +1532,10 @@
  112.95  
  112.96  (*strip off pairs of assumptions/parameters in parallel -- they are
  112.97    identical because of lifting*)
  112.98 -fun strip_assums2 (Const("==>", _) $ _ $ B1,
  112.99 -                   Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
 112.100 -  | strip_assums2 (Const("all",_)$Abs(a,T,t1),
 112.101 -                   Const("all",_)$Abs(_,_,t2)) =
 112.102 +fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1,
 112.103 +                   Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2)
 112.104 +  | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1),
 112.105 +                   Const("Pure.all",_)$Abs(_,_,t2)) =
 112.106        let val (B1,B2) = strip_assums2 (t1,t2)
 112.107        in  (Abs(a,T,B1), Abs(a,T,B2))  end
 112.108    | strip_assums2 BB = BB;
 112.109 @@ -1543,13 +1543,13 @@
 112.110  
 112.111  (*Faster normalization: skip assumptions that were lifted over*)
 112.112  fun norm_term_skip env 0 t = Envir.norm_term env t
 112.113 -  | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
 112.114 +  | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) =
 112.115        let
 112.116          val T' = Envir.subst_type (Envir.type_env env) T
 112.117          (*Must instantiate types of parameters because they are flattened;
 112.118            this could be a NEW parameter*)
 112.119        in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
 112.120 -  | norm_term_skip env n (Const ("==>", _) $ A $ B) =
 112.121 +  | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) =
 112.122        Logic.mk_implies (A, norm_term_skip env (n - 1) B)
 112.123    | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
 112.124  
   113.1 --- a/src/Sequents/simpdata.ML	Fri Mar 21 15:36:00 2014 +0000
   113.2 +++ b/src/Sequents/simpdata.ML	Fri Mar 21 20:39:54 2014 +0100
   113.3 @@ -29,7 +29,7 @@
   113.4  
   113.5  (*Make meta-equalities.*)
   113.6  fun mk_meta_eq ctxt th = case concl_of th of
   113.7 -    Const("==",_)$_$_           => th
   113.8 +    Const(@{const_name Pure.eq},_)$_$_ => th
   113.9    | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
  113.10          (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
  113.11               ([], [p]) =>
   114.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 21 15:36:00 2014 +0000
   114.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 21 20:39:54 2014 +0100
   114.3 @@ -163,7 +163,7 @@
   114.4      val _ = if fastype_of t <> propT
   114.5        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
   114.6        else ();
   114.7 -    val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
   114.8 +    val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
   114.9      val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
  114.10       of SOME Holds => true
  114.11        | _ => false;
   115.1 --- a/src/Tools/Code/code_symbol.ML	Fri Mar 21 15:36:00 2014 +0000
   115.2 +++ b/src/Tools/Code/code_symbol.ML	Fri Mar 21 20:39:54 2014 +0100
   115.3 @@ -88,8 +88,8 @@
   115.4  in
   115.5  
   115.6  fun default_base (Constant "") = "value"
   115.7 -  | default_base (Constant "==>") = "follows"
   115.8 -  | default_base (Constant "==") = "meta_eq"
   115.9 +  | default_base (Constant @{const_name Pure.imp}) = "follows"
  115.10 +  | default_base (Constant @{const_name Pure.eq}) = "meta_eq"
  115.11    | default_base (Constant c) = base c
  115.12    | default_base (Type_Constructor tyco) = base tyco
  115.13    | default_base (Type_Class class) = base class
   116.1 --- a/src/Tools/Code/code_thingol.ML	Fri Mar 21 15:36:00 2014 +0000
   116.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Mar 21 20:39:54 2014 +0100
   116.3 @@ -800,8 +800,8 @@
   116.4      val ty = fastype_of t;
   116.5      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   116.6        o dest_TFree))) t [];
   116.7 -    val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
   116.8 -    val dummy_constant = Constant @{const_name dummy_pattern};
   116.9 +    val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
  116.10 +    val dummy_constant = Constant @{const_name Pure.dummy_pattern};
  116.11      val stmt_value =
  116.12        fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
  116.13        ##>> translate_typ ctxt algbr eqngr false ty
  116.14 @@ -818,7 +818,7 @@
  116.15          val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
  116.16        in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
  116.17    in
  116.18 -    ensure_stmt Constant stmt_value @{const_name dummy_pattern}
  116.19 +    ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
  116.20      #> snd
  116.21      #> term_value
  116.22    end;
   117.1 --- a/src/Tools/induct.ML	Fri Mar 21 15:36:00 2014 +0000
   117.2 +++ b/src/Tools/induct.ML	Fri Mar 21 20:39:54 2014 +0100
   117.3 @@ -162,7 +162,7 @@
   117.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
   117.5  
   117.6  val rearrange_eqs_simproc =
   117.7 -  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
   117.8 +  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
   117.9      (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
  117.10  
  117.11  
  117.12 @@ -644,14 +644,16 @@
  117.13  
  117.14  local
  117.15  
  117.16 -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
  117.17 +fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) =
  117.18 +      c $ Abs (a, T, goal_prefix k B)
  117.19    | goal_prefix 0 _ = Term.dummy_prop
  117.20 -  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
  117.21 +  | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) =
  117.22 +      c $ A $ goal_prefix (k - 1) B
  117.23    | goal_prefix _ _ = Term.dummy_prop;
  117.24  
  117.25 -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
  117.26 +fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1
  117.27    | goal_params 0 _ = 0
  117.28 -  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
  117.29 +  | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B
  117.30    | goal_params _ _ = 0;
  117.31  
  117.32  fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
  117.33 @@ -670,11 +672,13 @@
  117.34            [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
  117.35             (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
  117.36  
  117.37 -    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
  117.38 +    fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
  117.39 +          goal_concl k ((a, T) :: xs) B
  117.40        | goal_concl 0 xs B =
  117.41            if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
  117.42            else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
  117.43 -      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
  117.44 +      | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) =
  117.45 +          goal_concl (k - 1) xs B
  117.46        | goal_concl _ _ _ = NONE;
  117.47    in
  117.48      (case goal_concl n [] goal of
   118.1 --- a/src/Tools/misc_legacy.ML	Fri Mar 21 15:36:00 2014 +0000
   118.2 +++ b/src/Tools/misc_legacy.ML	Fri Mar 21 20:39:54 2014 +0100
   118.3 @@ -130,9 +130,9 @@
   118.4      H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   118.5    Main difference from strip_assums concerns parameters:
   118.6      it replaces the bound variables by free variables.  *)
   118.7 -fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
   118.8 +fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) =
   118.9        strip_context_aux (params, H :: Hs, B)
  118.10 -  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
  118.11 +  | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) =
  118.12        let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
  118.13        in strip_context_aux ((b, T) :: params, Hs, u) end
  118.14    | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   119.1 --- a/src/Tools/nbe.ML	Fri Mar 21 15:36:00 2014 +0000
   119.2 +++ b/src/Tools/nbe.ML	Fri Mar 21 20:39:54 2014 +0100
   119.3 @@ -586,7 +586,7 @@
   119.4    let
   119.5      val thy = Proof_Context.theory_of ctxt;
   119.6      val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
   119.7 -    val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
   119.8 +    val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
   119.9      val rhs = Thm.cterm_of thy raw_rhs;
  119.10    in Thm.mk_binop eq lhs rhs end;
  119.11  
   120.1 --- a/src/Tools/quickcheck.ML	Fri Mar 21 15:36:00 2014 +0000
   120.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 21 20:39:54 2014 +0100
   120.3 @@ -358,7 +358,7 @@
   120.4      val lthy = Proof.context_of state;
   120.5      val thy = Proof.theory_of state;
   120.6      val _ = message lthy "Quickchecking..."
   120.7 -    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
   120.8 +    fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
   120.9        | strip t = t;
  120.10      val {goal = st, ...} = Proof.raw_goal state;
  120.11      val (gi, frees) = Logic.goal_params (prop_of st) i;
   121.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Mar 21 15:36:00 2014 +0000
   121.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Mar 21 20:39:54 2014 +0100
   121.3 @@ -244,21 +244,20 @@
   121.4    fun add_recursor thy =
   121.5      if need_recursor then
   121.6        thy
   121.7 -      |> Sign.add_consts_i
   121.8 -        [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
   121.9 +      |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
  121.10        |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
  121.11      else thy;
  121.12  
  121.13    val (con_defs, thy0) = thy_path
  121.14 -             |> Sign.add_consts_i
  121.15 -                 (map (fn (c, T, mx) => (Binding.name c, T, mx))
  121.16 -                  ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
  121.17 -             |> Global_Theory.add_defs false
  121.18 -                 (map (Thm.no_attributes o apfst Binding.name)
  121.19 -                  (case_def ::
  121.20 -                   flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
  121.21 -             ||> add_recursor
  121.22 -             ||> Sign.parent_path
  121.23 +    |> Sign.add_consts
  121.24 +        (map (fn (c, T, mx) => (Binding.name c, T, mx))
  121.25 +         ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
  121.26 +    |> Global_Theory.add_defs false
  121.27 +        (map (Thm.no_attributes o apfst Binding.name)
  121.28 +         (case_def ::
  121.29 +          flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
  121.30 +    ||> add_recursor
  121.31 +    ||> Sign.parent_path;
  121.32  
  121.33    val intr_names = map (Binding.name o #2) (flat con_ty_lists);
  121.34    val (thy1, ind_result) =