# HG changeset patch # User wenzelm # Date 1395430794 -3600 # Node ID 2b2bcf4ecb48240183d094b818b603d0bfb5bdd1 # Parent 5d147e1e18d11173d4eb316420b20634c54ae2a4# Parent 84fc7dfa3cd439a5eace985db3c7fa84b241b83d merged diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 NEWS --- a/NEWS Fri Mar 21 15:36:00 2014 +0000 +++ b/NEWS Fri Mar 21 20:39:54 2014 +0100 @@ -71,6 +71,34 @@ *** Pure *** +* Basic constants of Pure use more conventional names and are always +qualified. Rare INCOMPATIBILITY, but with potentially serious +consequences, notably for tools in Isabelle/ML. The following +renaming needs to be applied: + + == ~> Pure.eq + ==> ~> Pure.imp + all ~> Pure.all + TYPE ~> Pure.type + dummy_pattern ~> Pure.dummy_pattern + +Systematic porting works by using the following theory setup on a +*previous* Isabelle version to introduce the new name accesses for the +old constants: + +setup {* + fn thy => thy + |> Sign.root_path + |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "==" + |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>" + |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all" + |> Sign.restore_naming thy +*} + +Thus ML antiquotations like @{const_name Pure.eq} may be used already. +Later the application is moved to the current Isabelle version, and +the auxiliary aliases are deleted. + * Low-level type-class commands 'classes', 'classrel', 'arities' have been discontinued to avoid the danger of non-trivial axiomatization that is not immediately visible. INCOMPATIBILITY, use regular diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/CCL/Wfd.thy Fri Mar 21 20:39:54 2014 +0100 @@ -423,10 +423,10 @@ @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @ @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs}; -fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l) +fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l) | bvars _ l = l -fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t +fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Doc/Codegen/Setup.thy --- a/src/Doc/Codegen/Setup.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Doc/Codegen/Setup.thy Fri Mar 21 20:39:54 2014 +0100 @@ -19,10 +19,10 @@ let val typ = Simple_Syntax.read_typ; in - Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + Sign.del_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + Sign.add_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Doc/IsarImplementation/Logic.thy Fri Mar 21 20:39:54 2014 +0100 @@ -850,7 +850,7 @@ @{text "#A \ A"} \\[1ex] @{text "term :: \ \ prop"} & (prefix @{text "TERM"}) \\ @{text "term x \ (\A. A \ A)"} \\[1ex] - @{text "TYPE :: \ itself"} & (prefix @{text "TYPE"}) \\ + @{text "type :: \ itself"} & (prefix @{text "TYPE"}) \\ @{text "(unspecified)"} \\ \end{tabular} \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Doc/ProgProve/LaTeXsugar.thy --- a/src/Doc/ProgProve/LaTeXsugar.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Doc/ProgProve/LaTeXsugar.thy Fri Mar 21 20:39:54 2014 +0100 @@ -13,7 +13,7 @@ (* THEOREMS *) notation (Rule output) - "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") + Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" @@ -28,7 +28,7 @@ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") notation (IfThen output) - "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") @@ -36,7 +36,7 @@ "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") notation (IfThenNoBox output) - "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/FOL/simpdata.ML Fri Mar 21 20:39:54 2014 +0100 @@ -14,7 +14,7 @@ error("conclusion must be a =-equality or <->");; fun mk_eq th = case concl_of th of - Const("==",_)$_$_ => th + Const(@{const_name Pure.eq},_)$_$_ => th | _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th | _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/FOLP/hypsubst.ML Fri Mar 21 20:39:54 2014 +0100 @@ -58,8 +58,8 @@ assumption. Returns the number of intervening assumptions, paried with the rule asm_rl (resp. sym). *) fun eq_var bnd = - let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t - | eq_var_aux k (Const("==>",_) $ A $ B) = + let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t + | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) = ((k, inspect_pair bnd (dest_eq A)) (*Exception Match comes from inspect_pair or dest_eq*) handle Match => eq_var_aux (k+1) B) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/FOLP/simp.ML Fri Mar 21 20:39:54 2014 +0100 @@ -405,10 +405,10 @@ else (); (* Skip the first n hyps of a goal, and return the rest in generalized form *) -fun strip_varify(Const("==>", _) $ H $ B, n, vs) = +fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) = if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) else strip_varify(B,n-1,vs) - | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) = + | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) = strip_varify(t,n,Var(("?",length vs),T)::vs) | strip_varify _ = []; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Code_Evaluation.thy Fri Mar 21 20:39:54 2014 +0100 @@ -85,8 +85,9 @@ begin definition - "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') - [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" + "term_of (f \ 'a \ 'b) = + Const (STR ''Pure.dummy_pattern'') + (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" instance .. diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 21 20:39:54 2014 +0100 @@ -84,7 +84,7 @@ (* The result of the quantifier elimination *) val (th, tac) = (case (prop_of pre_thm) of - Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => + Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1)) in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 21 20:39:54 2014 +0100 @@ -64,7 +64,7 @@ fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) val (th, tac) = case prop_of pre_thm of - Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => + Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => let val pth = linr_oracle (ctxt, Envir.eta_long [] t1) in ((pth RS iffD2) RS pre_thm, diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Mar 21 20:39:54 2014 +0100 @@ -184,9 +184,9 @@ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm - | Const ("==>", _) $ _ $ _ => find_args bounds tm - | Const ("==", _) $ _ $ _ => find_args bounds tm - | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm + | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm + | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm) | _ => Thm.dest_fun2 tm) and find_args bounds tm = diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Decision_Procs/langford.ML Fri Mar 21 20:39:54 2014 +0100 @@ -204,13 +204,13 @@ else Thm.dest_fun2 tm | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm) | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm) - | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm - | Const ("==>", _) $ _ $ _ => find_args bounds tm - | Const ("==", _) $ _ $ _ => find_args bounds tm + | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm + | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm) | _ => Thm.dest_fun2 tm) and find_args bounds tm = @@ -230,7 +230,7 @@ fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let - fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} + fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"} fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t) val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 21 20:39:54 2014 +0100 @@ -112,7 +112,7 @@ fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) val (th, tac) = case (prop_of pre_thm) of - Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => + Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => let val pth = (* If quick_and_dirty then run without proof generation as oracle*) if Config.get ctxt quick_and_dirty diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 21 20:39:54 2014 +0100 @@ -143,7 +143,7 @@ case lhs of Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) => mk_eqn (f, big_lambda x rhs) - | f $ Const (@{const_name TYPE}, T) => + | f $ Const (@{const_name Pure.type}, T) => mk_eqn (f, Abs ("t", T, rhs)) | Const _ => Logic.mk_equals (lhs, rhs) | _ => raise TERM ("lhs not of correct form", [lhs, rhs]) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Fri Mar 21 20:39:54 2014 +0100 @@ -80,7 +80,7 @@ val transformed_decls = map (transform thy) contconst_decls in thy - |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) + |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |> Sign.add_trrules (maps #3 transformed_decls) end diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 20:39:54 2014 +0100 @@ -12,10 +12,10 @@ let val typ = Simple_Syntax.read_typ; in - Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + Sign.del_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + Sign.add_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Import/import_rule.ML Fri Mar 21 20:39:54 2014 +0100 @@ -172,7 +172,7 @@ let val rhs = term_of rhs val typ = type_of rhs - val thy1 = Sign.add_consts_i [(Binding.name constname, typ, NoSyn)] thy + val thy1 = Sign.add_consts [(Binding.name constname, typ, NoSyn)] thy val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs) val (thms, thy2) = Global_Theory.add_defs false [((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1 diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Library/Countable.thy Fri Mar 21 20:39:54 2014 +0100 @@ -275,7 +275,7 @@ let val ty_name = (case goal of - (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n + (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n | _ => raise Match) val typedef_info = hd (Typedef.get_info ctxt ty_name) val typedef_thm = #type_definition (snd typedef_info) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Library/LaTeXsugar.thy Fri Mar 21 20:39:54 2014 +0100 @@ -67,7 +67,7 @@ (* THEOREMS *) notation (Rule output) - "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") + Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" @@ -82,7 +82,7 @@ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") notation (IfThen output) - "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") @@ -90,7 +90,7 @@ "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") notation (IfThenNoBox output) - "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Library/OptionalSugar.thy Fri Mar 21 20:39:54 2014 +0100 @@ -33,7 +33,7 @@ (* aligning equations *) notation (tab output) "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and - "==" ("(_) \<^raw:}\putisatab\isa{\ >\\<^raw:}\putisatab\isa{> (_)") + "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\\<^raw:}\putisatab\isa{> (_)") (* Let *) translations diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Library/bnf_decl.ML --- a/src/HOL/Library/bnf_decl.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Library/bnf_decl.ML Fri Mar 21 20:39:54 2014 +0100 @@ -57,7 +57,7 @@ (if nwits = 1 then [0] else 1 upto nwits); val lthy = Local_Theory.background_theory - (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: + (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) lthy; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Library/refute.ML Fri Mar 21 20:39:54 2014 +0100 @@ -545,10 +545,10 @@ fun unfold_loop t = case t of (* Pure *) - Const (@{const_name all}, _) => t - | Const (@{const_name "=="}, _) => t - | Const (@{const_name "==>"}, _) => t - | Const (@{const_name TYPE}, _) => t (* axiomatic type classes *) + Const (@{const_name Pure.all}, _) => t + | Const (@{const_name Pure.eq}, _) => t + | Const (@{const_name Pure.imp}, _) => t + | Const (@{const_name Pure.type}, _) => t (* axiomatic type classes *) (* HOL *) | Const (@{const_name Trueprop}, _) => t | Const (@{const_name Not}, _) => t @@ -709,11 +709,11 @@ and collect_term_axioms t axs = case t of (* Pure *) - Const (@{const_name all}, _) => axs - | Const (@{const_name "=="}, _) => axs - | Const (@{const_name "==>"}, _) => axs + Const (@{const_name Pure.all}, _) => axs + | Const (@{const_name Pure.eq}, _) => axs + | Const (@{const_name Pure.imp}, _) => axs (* axiomatic type classes *) - | Const (@{const_name TYPE}, T) => collect_type_axioms T axs + | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs (* HOL *) | Const (@{const_name Trueprop}, _) => axs | Const (@{const_name Not}, _) => axs @@ -1183,7 +1183,7 @@ (* interpretation which includes values for the (formerly) *) (* quantified variables. *) (* maps !!x1...xn. !xk...xm. t to t *) - fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = + fun strip_all_body (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip_all_body t | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = strip_all_body t @@ -1191,7 +1191,7 @@ strip_all_body t | strip_all_body t = t (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) - fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = + fun strip_all_vars (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = strip_all_vars t @@ -1569,7 +1569,7 @@ fun Pure_interpreter ctxt model args t = case t of - Const (@{const_name all}, _) $ t1 => + Const (@{const_name Pure.all}, _) $ t1 => let val (i, m, a) = interpret ctxt model args t1 in @@ -1584,11 +1584,11 @@ end | _ => raise REFUTE ("Pure_interpreter", - "\"all\" is followed by a non-function") + "\"Pure.all\" is followed by a non-function") end - | Const (@{const_name all}, _) => + | Const (@{const_name Pure.all}, _) => SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) $ t1 $ t2 => + | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 @@ -1597,11 +1597,11 @@ SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end - | Const (@{const_name "=="}, _) $ _ => + | Const (@{const_name Pure.eq}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) => + | Const (@{const_name Pure.eq}, _) => SOME (interpret ctxt model args (eta_expand t 2)) - | Const (@{const_name "==>"}, _) $ t1 $ t2 => + | Const (@{const_name Pure.imp}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret ctxt model args t1 @@ -1611,9 +1611,9 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name "==>"}, _) $ _ => + | Const (@{const_name Pure.imp}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "==>"}, _) => + | Const (@{const_name Pure.imp}, _) => SOME (interpret ctxt model args (eta_expand t 2)) | _ => NONE; @@ -1632,7 +1632,7 @@ (* redundant, since 'False' is also an IDT constructor *) | Const (@{const_name False}, _) => SOME (FF, model, args) - | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) + | Const (@{const_name All}, _) $ t1 => (* similar to "Pure.all" *) let val (i, m, a) = interpret ctxt model args t1 in @@ -1670,7 +1670,7 @@ end | Const (@{const_name Ex}, _) => SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) + | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to Pure.eq *) let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 @@ -1715,7 +1715,7 @@ (* this would make "undef" propagate, even for formulae like *) (* "True | undef": *) (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) - | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) + | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to Pure.imp *) (* 3-valued logic *) let val (i1, m1, a1) = interpret ctxt model args t1 diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/List.thy --- a/src/HOL/List.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/List.thy Fri Mar 21 20:39:54 2014 +0100 @@ -439,7 +439,7 @@ val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; val case2 = Syntax.const @{syntax_const "_case1"} $ - Syntax.const @{const_syntax dummy_pattern} $ NilC; + Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC; val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Mar 21 20:39:54 2014 +0100 @@ -435,7 +435,8 @@ val ty = type_of a val (encoding, a) = remove_types encoding a val (encoding, b) = remove_types encoding b - val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding + val (eq, encoding) = + Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding in (encoding, EqPrem (a, b, ty, eq)) end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 20:39:54 2014 +0100 @@ -218,7 +218,7 @@ (@{const_name induct_conj}, "'a"),*) (@{const_name "undefined"}, "'a"), (@{const_name "default"}, "'a"), - (@{const_name "dummy_pattern"}, "'a::{}"), + (@{const_name "Pure.dummy_pattern"}, "'a::{}"), (@{const_name "HOL.simp_implies"}, "prop => prop => prop"), (@{const_name "bot_fun_inst.bot_fun"}, "'a"), (@{const_name "top_fun_inst.top_fun"}, "'a"), @@ -234,7 +234,7 @@ "nibble"] val forbidden_consts = - [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] + [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] fun is_forbidden_theorem (s, th) = let val consts = Term.add_const_names (prop_of th) [] in @@ -254,7 +254,7 @@ "HOL.induct_forall", @{const_name undefined}, @{const_name default}, - @{const_name dummy_pattern}, + @{const_name Pure.dummy_pattern}, @{const_name "HOL.simp_implies"}, @{const_name "bot_fun_inst.bot_fun"}, @{const_name "top_fun_inst.top_fun"}, @@ -275,7 +275,7 @@ @{const_name Quickcheck_Random.catch_match}, @{const_name Quickcheck_Exhaustive.unknown}, @{const_name Num.Bit0}, @{const_name Num.Bit1} - (*@{const_name "==>"}, @{const_name "=="}*)] + (*@{const_name Pure.imp}, @{const_name Pure.eq}*)] val forbidden_mutant_consts = [ diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Mar 21 20:39:54 2014 +0100 @@ -292,7 +292,7 @@ subsection {* Known Constants *} -lemma "x \ all \ False" +lemma "x \ Pure.all \ False" nitpick [card = 1, expect = genuine] nitpick [card = 1, box "('a \ prop) \ prop", expect = genuine] nitpick [card = 6, expect = genuine] @@ -306,15 +306,15 @@ nitpick [expect = genuine] oops -lemma "all (\x. Trueprop (f x y = f x y)) \ Trueprop True" +lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop True" nitpick [expect = none] by auto -lemma "all (\x. Trueprop (f x y = f x y)) \ Trueprop False" +lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop False" nitpick [expect = genuine] oops -lemma "I = (\x. x) \ all P \ all (\x. P (I x))" +lemma "I = (\x. x) \ Pure.all P \ Pure.all (\x. P (I x))" nitpick [expect = none] by auto diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Mar 21 20:39:54 2014 +0100 @@ -326,7 +326,7 @@ nitpick [expect = genuine] oops -lemma "(x \ all) \ False" +lemma "(x \ Pure.all) \ False" nitpick [expect = genuine] oops diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 21 20:39:54 2014 +0100 @@ -761,7 +761,7 @@ (Const (rep_name, T --> T') $ lhs, rhs)); val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> - Sign.add_consts_i [(cname', constrT, mx)] |> + Sign.add_consts [(cname', constrT, mx)] |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn]) end; @@ -1993,7 +1993,7 @@ val (reccomb_defs, thy12) = thy11 - |> Sign.add_consts_i (map (fn ((name, T), T') => + |> Sign.add_consts (map (fn ((name, T), T') => (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 20:39:54 2014 +0100 @@ -32,8 +32,8 @@ fun unquantify t = let - val (vs, Ts) = split_list (strip_qnt_vars "all" t); - val body = strip_qnt_body "all" t; + val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} t); + val body = strip_qnt_body @{const_name Pure.all} t; val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])) in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 20:39:54 2014 +0100 @@ -134,7 +134,7 @@ val thy = Context.theory_of context val thms_to_be_added = (case (prop_of orig_thm) of (* case: eqvt-lemma is of the implicational form *) - (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) => + (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) => let val (pi,typi) = get_pi concl thy in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Product_Type.thy Fri Mar 21 20:39:54 2014 +0100 @@ -457,7 +457,7 @@ ML {* (* replace parameters of product type by individual component parameters *) local (* filtering with exists_paired_all is an essential optimization *) - fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = + fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = can HOLogic.dest_prodT T orelse exists_paired_all t | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u | exists_paired_all (Abs (_, _, t)) = exists_paired_all t diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Prolog/prolog.ML Fri Mar 21 20:39:54 2014 +0100 @@ -13,9 +13,9 @@ Const(@{const_name Trueprop},_)$t => isD t | Const(@{const_name HOL.conj} ,_)$l$r => isD l andalso isD r | Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r - | Const( "==>",_)$l$r => isG l andalso isD r + | Const(@{const_name Pure.imp},_)$l$r => isG l andalso isD r | Const(@{const_name All},_)$Abs(s,_,t) => isD t - | Const("all",_)$Abs(s,_,t) => isD t + | Const(@{const_name Pure.all},_)$Abs(s,_,t) => isD t | Const(@{const_name HOL.disj},_)$_$_ => false | Const(@{const_name Ex} ,_)$_ => false | Const(@{const_name Not},_)$_ => false @@ -33,9 +33,9 @@ | Const(@{const_name HOL.conj} ,_)$l$r => isG l andalso isG r | Const(@{const_name HOL.disj} ,_)$l$r => isG l andalso isG r | Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r - | Const( "==>",_)$l$r => isD l andalso isG r + | Const(@{const_name Pure.imp},_)$l$r => isD l andalso isG r | Const(@{const_name All},_)$Abs(_,_,t) => isG t - | Const("all",_)$Abs(_,_,t) => isG t + | Const(@{const_name Pure.all},_)$Abs(_,_,t) => isG t | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t | Const(@{const_name True},_) => true | Const(@{const_name Not},_)$_ => false @@ -79,8 +79,8 @@ | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) | ap t = (0,false,t); (* - fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t - | rep_goal (Const ("==>",_)$s$t) = + fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t + | rep_goal (Const (@{const_name Pure.imp},_)$s$t) = (case rep_goal t of (l,t) => (s::l,t)) | rep_goal t = ([] ,t); val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Mar 21 20:39:54 2014 +0100 @@ -1001,7 +1001,7 @@ in (c, ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt), - Sign.add_consts_i [(b, T, NoSyn)] thy)) + Sign.add_consts [(b, T, NoSyn)] thy)) end; fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 21 20:39:54 2014 +0100 @@ -320,7 +320,7 @@ |> apfst the_single end -(*like strip_top_All_vars but for "all" instead of "All"*) +(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*) fun strip_top_all_vars acc t = if Logic.is_all t then let diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 21 20:39:54 2014 +0100 @@ -1670,7 +1670,7 @@ (* @{const_name HOL.not_equal}, *) @{const_name HOL.False}, @{const_name HOL.True}, - @{const_name "==>"}] + @{const_name Pure.imp}] fun strip_qtfrs_tac ctxt = REPEAT_DETERM (HEADGOAL (rtac @{thm allI})) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 20:39:54 2014 +0100 @@ -404,8 +404,9 @@ (* These are ignored anyway by the relevance filter (unless they appear in higher-order places) but not by the monomorphizer. *) val atp_logical_consts = - [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"}, - @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, + [@{const_name Pure.prop}, @{const_name Pure.conjunction}, + @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq}, + @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] (* These are either simplified away by "Meson.presimplify" (most of the time) or @@ -437,7 +438,7 @@ val tvar_a = TVar tvar_a_z val tvar_a_name = tvar_name tvar_a_z val itself_name = `make_fixed_type_const @{type_name itself} -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE} +val TYPE_name = `(make_fixed_const NONE) @{const_name Pure.type} val tvar_a_atype = AType ((tvar_a_name, []), []) val a_itself_atype = AType ((itself_name, []), [tvar_a_atype]) @@ -1879,8 +1880,8 @@ in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t - | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t - | s_not_prop t = @{const "==>"} $ t $ @{prop False} + | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t + | s_not_prop t = @{const Pure.imp} $ t $ @{prop False} fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 21 20:39:54 2014 +0100 @@ -46,7 +46,7 @@ fun hhf_concl_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name all}, _) $ Abs _ => + Const (@{const_name Pure.all}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct | _ => Conv.concl_conv ~1 cv ct); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 20:39:54 2014 +0100 @@ -86,8 +86,8 @@ | retype_free _ t = raise TERM ("retype_free", [t]); fun drop_all t = - subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev, - strip_qnt_body @{const_name all} t); + subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev, + strip_qnt_body @{const_name Pure.all} t); fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Mar 21 20:39:54 2014 +0100 @@ -149,7 +149,7 @@ | abs_pat _ _ = I; (* replace occurrences of dummy_pattern by distinct variables *) - fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used = + fun replace_dummies (Const (@{const_syntax Pure.dummy_pattern}, T)) used = let val (x, used') = variant_free "x" used in (Free (x, T), used') end | replace_dummies (t $ u) used = diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Mar 21 20:39:54 2014 +0100 @@ -237,7 +237,7 @@ HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs)); val ([def_thm], thy') = thy - |> Sign.add_consts_i [(cname', constrT, mx)] + |> Sign.add_consts [(cname', constrT, mx)] |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; @@ -262,7 +262,7 @@ val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = fold dt_constr_defs (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax) - (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []); + (thy3 |> Sign.add_consts iso_decls |> Sign.parent_path, [], [], [], []); (*********** isomorphisms for new types (introduced by typedef) ***********) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Datatype/primrec.ML --- a/src/HOL/Tools/Datatype/primrec.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Datatype/primrec.ML Fri Mar 21 20:39:54 2014 +0100 @@ -34,8 +34,8 @@ fun process_eqn is_fixed spec rec_fns = let - val (vs, Ts) = split_list (strip_qnt_vars "all" spec); - val body = strip_qnt_body "all" spec; + val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec); + val body = strip_qnt_body @{const_name Pure.all} spec; val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])); val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 20:39:54 2014 +0100 @@ -226,7 +226,7 @@ val (reccomb_defs, thy2) = thy1 - |> Sign.add_consts_i (map (fn ((name, T), T') => + |> Sign.add_consts (map (fn ((name, T), T') => (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (Global_Theory.add_defs false o map Thm.no_attributes) @@ -434,7 +434,7 @@ let fun prove_case_cong ((t, nchotomy), case_rewrites) = let - val Const ("==>", _) $ tm $ _ = t; + val Const (@{const_name Pure.imp}, _) $ tm $ _ = t; val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm; val cert = cterm_of thy; val nchotomy' = nchotomy RS spec; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Function/function_common.ML Fri Mar 21 20:39:54 2014 +0100 @@ -280,8 +280,8 @@ fun split_def ctxt check_head geq = let fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] - val qs = Term.strip_qnt_vars "all" geq - val imp = Term.strip_qnt_body "all" geq + val qs = Term.strip_qnt_vars @{const_name Pure.all} geq + val imp = Term.strip_qnt_body @{const_name Pure.all} geq val (gs, eq) = Logic.strip_horn imp val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Mar 21 20:39:54 2014 +0100 @@ -40,7 +40,7 @@ (* Removes all quantifiers from a term, replacing bound variables by frees. *) -fun dest_all_all (t as (Const ("all",_) $ _)) = +fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) = let val (v,b) = Logic.dest_all t |> apfst Free val (vs, b') = dest_all_all b diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Function/size.ML Fri Mar 21 20:39:54 2014 +0100 @@ -134,7 +134,7 @@ val ((size_def_thms, size_def_thms'), thy') = thy - |> Sign.add_consts_i (map (fn (s, T) => + |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) (size_names ~~ recTs1)) |> Global_Theory.add_defs false diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 21 20:39:54 2014 +0100 @@ -547,11 +547,11 @@ fun rename_to_tnames ctxt term = let - fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t + fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t | all_typs _ = [] - fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = - (Const ("all", T1) $ Abs (new_name, T2, rename t names)) + fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = + (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) | rename t _ = t val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 21 20:39:54 2014 +0100 @@ -105,7 +105,7 @@ try (fn () => let val thy = theory_of_thm thA val tmA = concl_of thA - val Const("==>",_) $ tmB $ _ = prop_of thB + val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB val tenv = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) |> snd @@ -472,7 +472,7 @@ (***** MESON PROOF PROCEDURE *****) -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi, +fun rhyps (Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ phi, As) = rhyps(phi, A::As) | rhyps (_, As) = As; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 21 20:39:54 2014 +0100 @@ -242,7 +242,7 @@ fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t = case t of (t1 as Const (s, _)) $ Abs (s', T, t') => - if s = @{const_name all} orelse s = @{const_name All} orelse + if s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex} then let val skolem = (pos = (s = @{const_name Ex})) @@ -254,7 +254,7 @@ else t | (t1 as Const (s, _)) $ t2 $ t3 => - if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then + if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3 else if s = @{const_name HOL.conj} orelse s = @{const_name HOL.disj} then @@ -275,13 +275,13 @@ ct |> (case term_of ct of Const (s, _) $ Abs (s', _, _) => - if s = @{const_name all} orelse s = @{const_name All} orelse + if s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex} then Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos else Conv.all_conv | Const (s, _) $ _ $ _ => - if s = @{const_name "==>"} orelse s = @{const_name implies} then + if s = @{const_name Pure.imp} orelse s = @{const_name implies} then Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) else if s = @{const_name conj} orelse s = @{const_name disj} then Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 21 20:39:54 2014 +0100 @@ -1062,7 +1062,7 @@ end fun is_fixed_equation ctxt - (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = + (Const (@{const_name Pure.eq}, _) $ Free (s, _) $ Const _) = Variable.is_fixed ctxt s | is_fixed_equation _ _ = false diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 20:39:54 2014 +0100 @@ -363,9 +363,9 @@ "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as well. *) val built_in_consts = - [(@{const_name all}, 1), - (@{const_name "=="}, 2), - (@{const_name "==>"}, 2), + [(@{const_name Pure.all}, 1), + (@{const_name Pure.eq}, 2), + (@{const_name Pure.imp}, 2), (@{const_name Pure.conjunction}, 2), (@{const_name Trueprop}, 1), (@{const_name Not}, 1), @@ -973,7 +973,7 @@ fold (fn (z as ((s, _), T)) => fn t' => Logic.all_const T $ Abs (s, T, abstract_over (Var z, t'))) (take (length zs' - length zs) zs') - fun aux zs (@{const "==>"} $ t1 $ t2) = + fun aux zs (@{const Pure.imp} $ t1 $ t2) = let val zs' = Term.add_vars t1 zs in close_up zs zs' (Logic.mk_implies (t1, aux zs' t2)) end @@ -1178,7 +1178,7 @@ | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1) | loose_bvar1_count _ = 0 -fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) = +fun s_betapply _ (t1 as Const (@{const_name Pure.eq}, _) $ t1', t2) = if t1' aconv t2 then @{prop True} else t1 $ t2 | s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) = if t1' aconv t2 then @{term True} else t1 $ t2 @@ -1422,8 +1422,8 @@ simplification rules (equational specifications). *) fun term_under_def t = case t of - @{const "==>"} $ _ $ t2 => term_under_def t2 - | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1 + @{const Pure.imp} $ _ $ t2 => term_under_def t2 + | Const (@{const_name Pure.eq}, _) $ t1 $ _ => term_under_def t1 | @{const Trueprop} $ t1 => term_under_def t1 | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1 | Abs (_, _, t') => term_under_def t' @@ -1444,11 +1444,11 @@ fun normalized_rhs_of t = let fun aux (v as Var _) (SOME t) = SOME (lambda v t) - | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t) + | aux (c as Const (@{const_name Pure.type}, _)) (SOME t) = SOME (lambda c t) | aux _ _ = NONE val (lhs, rhs) = case t of - Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2) + Const (@{const_name Pure.eq}, _) $ t1 $ t2 => (t1, t2) | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) => (t1, t2) | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) @@ -1527,9 +1527,9 @@ fun lhs_of_equation t = case t of - Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 - | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1 - | @{const "==>"} $ _ $ t2 => lhs_of_equation t2 + Const (@{const_name Pure.all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 + | Const (@{const_name Pure.eq}, _) $ t1 $ _ => SOME t1 + | @{const Pure.imp} $ _ $ t2 => lhs_of_equation t2 | @{const Trueprop} $ t1 => lhs_of_equation t1 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1 | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1 @@ -1947,7 +1947,7 @@ @{const Trueprop} $ extensional_equal j T t1 t2 | @{const Trueprop} $ t' => @{const Trueprop} $ HOLogic.mk_eq (t', @{const True}) - | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => + | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 => @{const Trueprop} $ extensional_equal j T t1 t2 | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^ quote (Syntax.string_of_term ctxt t) ^ "."); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 21 20:39:54 2014 +0100 @@ -844,8 +844,8 @@ if not (could_exist_alpha_subtype alpha_T T) then (mtype_for T, accum) else case s of - @{const_name all} => do_all T accum - | @{const_name "=="} => do_equals T accum + @{const_name Pure.all} => do_all T accum + | @{const_name Pure.eq} => do_equals T accum | @{const_name All} => do_all T accum | @{const_name Ex} => let val set_T = domain_type T in @@ -1057,9 +1057,9 @@ " \ " ^ Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^ string_for_sign sn ^ "?"); case t of - Const (s as @{const_name all}, _) $ Abs (_, T1, t1) => + Const (s as @{const_name Pure.all}, _) $ Abs (_, T1, t1) => do_quantifier s T1 t1 - | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 + | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => do_equals t1 t2 | @{const Trueprop} $ t1 => do_formula sn t1 accum | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) => do_quantifier s T1 t1 @@ -1076,7 +1076,7 @@ do_formula sn (betapply (t2, t1)) accum | @{const Pure.conjunction} $ t1 $ t2 => do_connect meta_conj_spec false t1 t2 accum - | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum + | @{const Pure.imp} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum @@ -1122,11 +1122,11 @@ and do_implies t1 t2 = do_term t1 #> do_formula t2 and do_formula t accum = case t of - Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum + Const (@{const_name Pure.all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum | @{const Trueprop} $ t1 => do_formula t1 accum - | Const (@{const_name "=="}, _) $ t1 $ t2 => + | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => consider_general_equals mdata true t1 t2 accum - | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum + | @{const Pure.imp} $ t1 $ t2 => do_implies t1 t2 accum | @{const Pure.conjunction} $ t1 $ t2 => fold (do_formula) [t1, t2] accum | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Mar 21 20:39:54 2014 +0100 @@ -474,12 +474,12 @@ | k => sub (eta_expand Ts t k) in case strip_comb t of - (Const (@{const_name all}, _), [Abs (s, T, t1)]) => + (Const (@{const_name Pure.all}, _), [Abs (s, T, t1)]) => do_quantifier All s T t1 - | (t0 as Const (@{const_name all}, _), [t1]) => + | (t0 as Const (@{const_name Pure.all}, _), [t1]) => sub' (t0 $ eta_expand Ts t1 1) - | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2 - | (Const (@{const_name "==>"}, _), [t1, t2]) => + | (Const (@{const_name Pure.eq}, T), [t1, t2]) => sub_equals T t1 t2 + | (Const (@{const_name Pure.imp}, _), [t1, t2]) => Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2) | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) => Op2 (And, prop_T, Any, sub' t1, sub' t2) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 20:39:54 2014 +0100 @@ -36,9 +36,9 @@ val may_use_binary_ints = let - fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = + fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = aux def t1 andalso aux false t2 - | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 + | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def t2 | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = aux def t1 andalso aux false t2 | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 @@ -145,7 +145,7 @@ case t of @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z | Const (s0, _) $ t1 $ _ => - if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then + if s0 = @{const_name Pure.eq} orelse s0 = @{const_name HOL.eq} then let val (t', args) = strip_comb t1 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') @@ -187,12 +187,12 @@ end and do_term new_Ts old_Ts polar t = case t of - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => + Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) => do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 - | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => + | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 => do_equals new_Ts old_Ts s0 T0 t1 t2 - | @{const "==>"} $ t1 $ t2 => - @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 + | @{const Pure.imp} $ t1 $ t2 => + @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1 $ do_term new_Ts old_Ts polar t2 | @{const Pure.conjunction} $ t1 $ t2 => @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 @@ -334,9 +334,9 @@ val k = maxidx_of_term t + 1 fun do_term Ts def t args seen = case t of - (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => + (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 => do_eq_or_imp Ts true def t0 t1 t2 seen - | (t0 as @{const "==>"}) $ t1 $ t2 => + | (t0 as @{const Pure.imp}) $ t1 $ t2 => if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_eq_or_imp Ts true def t0 t1 t2 seen @@ -401,9 +401,9 @@ val num_occs_of_var = fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) | _ => I) t (K 0) - fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = + fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) = aux_eq Ts careful true t0 t1 t2 - | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) = + | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) = t0 $ aux Ts false t1 $ aux Ts careful t2 | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) = aux_eq Ts careful true t0 t1 t2 @@ -455,22 +455,22 @@ (** Destruction of universal and existential equalities **) -fun curry_assms (@{const "==>"} $ (@{const Trueprop} +fun curry_assms (@{const Pure.imp} $ (@{const Trueprop} $ (@{const HOL.conj} $ t1 $ t2)) $ t3) = curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) - | curry_assms (@{const "==>"} $ t1 $ t2) = - @{const "==>"} $ curry_assms t1 $ curry_assms t2 + | curry_assms (@{const Pure.imp} $ t1 $ t2) = + @{const Pure.imp} $ curry_assms t1 $ curry_assms t2 | curry_assms t = t val destroy_universal_equalities = let fun aux prems zs t = case t of - @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 + @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2 | _ => Logic.list_implies (rev prems, t) and aux_implies prems zs t1 t2 = case t1 of - Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 + Const (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') => aux_eq prems zs z t' t1 t2 | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) => @@ -591,10 +591,10 @@ not (is_higher_order_type abs_T)) polar t) in case t of - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => + Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 - | @{const "==>"} $ t1 $ t2 => - @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 + | @{const Pure.imp} $ t1 $ t2 => + @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1 $ aux ss Ts js skolemizable polar t2 | @{const Pure.conjunction} $ t1 $ t2 => @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1 @@ -654,7 +654,7 @@ (** Function specialization **) -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 +fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) = snd (strip_comb t1) @@ -866,7 +866,7 @@ if exists_subterm (curry (op aconv) u) def then NONE else SOME u in case t of - Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def + Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) => do_equals u def @@ -918,7 +918,7 @@ and add_def_axiom depth = add_axiom fst apfst true depth and add_nondef_axiom depth = add_axiom snd apsnd false depth and add_maybe_def_axiom depth t = - (if head_of t <> @{const "==>"} then add_def_axiom + (if head_of t <> @{const Pure.imp} then add_def_axiom else add_nondef_axiom) depth t and add_eq_axiom depth t = (if is_constr_pattern_formula ctxt t then add_def_axiom @@ -979,7 +979,7 @@ (Const (mate_of_rep_fun ctxt x)) |> fold (add_def_axiom depth) (inverse_axioms_for_rep_fun ctxt x) - else if s = @{const_name TYPE} then + else if s = @{const_name Pure.type} then accum else case def_of_const thy def_tables x of SOME _ => diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 21 20:39:54 2014 +0100 @@ -307,7 +307,8 @@ fun imp_prems_conv cv ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct + Const (@{const_name Pure.imp}, _) $ _ $ _ => + Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct | _ => Conv.all_conv ct) fun preprocess_intro thy rule = diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 20:39:54 2014 +0100 @@ -460,14 +460,14 @@ (* general syntactic functions *) -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true +fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = true | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true | is_equationlike_term _ = false val is_equationlike = is_equationlike_term o prop_of -fun is_pred_equation_term (Const ("==", _) $ u $ v) = +fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) = (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) | is_pred_equation_term _ = false @@ -620,7 +620,7 @@ (* fun equals_conv lhs_cv rhs_cv ct = case Thm.term_of ct of - Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct + Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct | _ => error "equals_conv" *) @@ -973,7 +973,8 @@ fun imp_prems_conv cv ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct + Const (@{const_name Pure.imp}, _) $ _ $ _ => + Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct | _ => Conv.all_conv ct) @@ -1212,7 +1213,7 @@ val constname = "quickcheck" val full_constname = Sign.full_bname thy constname val constT = map snd vs' ---> @{typ bool} - val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy + val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy val const = Const (full_constname, constT) val t = Logic.list_implies diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Mar 21 20:39:54 2014 +0100 @@ -1146,7 +1146,7 @@ val lhs = Const (mode_cname, funT) val def = Logic.mk_equals (lhs, predterm) val ([definition], thy') = thy |> - Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> + Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])] val ctxt' = Proof_Context.init_global thy' val rules as ((intro, elim), _) = @@ -1171,7 +1171,7 @@ val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode val funT = Comp_Mod.funT_of comp_modifiers mode T in - thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] + thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname end; in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Mar 21 20:39:54 2014 +0100 @@ -84,7 +84,7 @@ val is_introlike = is_introlike_term o prop_of -fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) = +fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) = (case strip_comb u of (Const (_, T), args) => if (length (binder_types T) = length args) then @@ -98,7 +98,7 @@ val check_equation_format = check_equation_format_term o prop_of -fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u) +fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u) | defining_term_of_equation_term t = raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) @@ -224,8 +224,8 @@ end val logic_operator_names = - [@{const_name "=="}, - @{const_name "==>"}, + [@{const_name Pure.eq}, + @{const_name Pure.imp}, @{const_name Trueprop}, @{const_name Not}, @{const_name HOL.eq}, diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 20:39:54 2014 +0100 @@ -284,7 +284,7 @@ end val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) val (intrs, thy') = thy - |> Sign.add_consts_i + |> Sign.add_consts (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn)) dst_preds) |> fold_map Specification.axiom (* FIXME !?!?!?! *) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Mar 21 20:39:54 2014 +0100 @@ -87,7 +87,7 @@ val lhs = list_comb (Const (full_constname, constT), params @ args) val def = Logic.mk_equals (lhs, atom) val ([definition], thy') = thy - |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] in (lhs, ((full_constname, [definition]) :: defs, thy')) @@ -119,7 +119,7 @@ Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs) val new_defs = map mk_def srs val (definition, thy') = thy - |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> fold_map Specification.axiom (* FIXME !?!?!?! *) (map_index (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs) @@ -245,7 +245,7 @@ val lhs = list_comb (const, frees) val def = Logic.mk_equals (lhs, abs_arg') val ([definition], thy') = thy - |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] in (list_comb (Logic.varify_global const, vars), diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Mar 21 20:39:54 2014 +0100 @@ -94,7 +94,7 @@ end handle Pattern.Unif => NONE) val specialised_intros_t = map_filter I (map specialise_intro intros) val thy' = - Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy + Sign.add_consts [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t val exported_intros = Variable.exportT ctxt' ctxt specialised_intros val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Mar 21 20:39:54 2014 +0100 @@ -795,7 +795,7 @@ fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let - fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} + fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"} fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t) val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 20:39:54 2014 +0100 @@ -428,7 +428,7 @@ fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = let val frees = Term.add_free_names t [] - val dummy_term = @{term "Code_Evaluation.Const (STR ''dummy_pattern'') + val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} val return = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ "term"} diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 21 20:39:54 2014 +0100 @@ -34,7 +34,7 @@ fun mk_partial_term_of (x, T) = Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of}, Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) - $ Const ("TYPE", Term.itselfT T) $ x + $ Logic.mk_type T $ x (** formal definition **) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 20:39:54 2014 +0100 @@ -52,7 +52,7 @@ (case Thm.prop_of thm of @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => norm_def (thm RS @{thm fun_cong}) - | Const (@{const_name "=="}, _) $ _ $ Abs _ => + | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) | _ => thm) @@ -61,20 +61,20 @@ fun atomize_conv ctxt ct = (case Thm.term_of ct of - @{const "==>"} $ _ $ _ => + @{const Pure.imp} $ _ $ _ => Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp} - | Const (@{const_name "=="}, _) $ _ $ _ => + | Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq} - | Const (@{const_name all}, _) $ Abs _ => + | Const (@{const_name Pure.all}, _) $ Abs _ => Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all} | _ => Conv.all_conv) ct val setup_atomize = - fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, - @{const_name "=="}, @{const_name all}, @{const_name Trueprop}] + fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, + @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}] (** unfold special quantifiers **) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT/smt_utils.ML Fri Mar 21 20:39:54 2014 +0100 @@ -188,7 +188,7 @@ @{const Trueprop} $ _ => Thm.dest_arg ct | _ => raise CTERM ("not a property", [ct])) -val equals = mk_const_pat @{theory} @{const_name "=="} destT1 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu val dest_prop = (fn @{const Trueprop} $ t => t | t => t) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Mar 21 20:39:54 2014 +0100 @@ -614,7 +614,7 @@ (* |- (EX x. P x) = P c |- ~(ALL x. P x) = ~ P c *) local val forall = - SMT_Utils.mk_const_pat @{theory} @{const_name all} + SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all} (SMT_Utils.destT1 o SMT_Utils.destT1) fun mk_forall cv ct = Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Mar 21 20:39:54 2014 +0100 @@ -199,7 +199,7 @@ and abstr (dcvs as (d, cvs)) ct = (case Thm.term_of ct of @{const Trueprop} $ _ => abstr1 dcvs ct - | @{const "==>"} $ _ $ _ => abstr2 dcvs ct + | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct | @{const True} => pair ct | @{const False} => pair ct | @{const Not} $ _ => abstr1 dcvs ct @@ -229,7 +229,7 @@ | _ => fresh_abstraction dcvs ct cx))) in abstr (depth, []) end -val cimp = Thm.cterm_of @{theory} @{const "==>"} +val cimp = Thm.cterm_of @{theory} @{const Pure.imp} fun deepen depth f x = if depth = 0 then f depth x diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT2/smt2_normalize.ML --- a/src/HOL/Tools/SMT2/smt2_normalize.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Fri Mar 21 20:39:54 2014 +0100 @@ -48,7 +48,7 @@ (case Thm.prop_of thm of @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => norm_def (thm RS @{thm fun_cong}) - | Const (@{const_name "=="}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) + | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) | _ => thm) @@ -56,17 +56,17 @@ fun atomize_conv ctxt ct = (case Thm.term_of ct of - @{const "==>"} $ _ $ _ => + @{const Pure.imp} $ _ $ _ => Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp} - | Const (@{const_name "=="}, _) $ _ $ _ => + | Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq} - | Const (@{const_name all}, _) $ Abs _ => + | Const (@{const_name Pure.all}, _) $ Abs _ => Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all} | _ => Conv.all_conv) ct val setup_atomize = - fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="}, - @{const_name all}, @{const_name Trueprop}] + fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq}, + @{const_name Pure.all}, @{const_name Trueprop}] (** unfold special quantifiers **) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT2/smt2_util.ML --- a/src/HOL/Tools/SMT2/smt2_util.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT2/smt2_util.ML Fri Mar 21 20:39:54 2014 +0100 @@ -185,7 +185,7 @@ @{const Trueprop} $ _ => Thm.dest_arg ct | _ => raise CTERM ("not a property", [ct])) -val equals = mk_const_pat @{theory} @{const_name "=="} destT1 +val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu val dest_prop = (fn @{const Trueprop} $ t => t | t => t) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT2/z3_new_proof.ML --- a/src/HOL/Tools/SMT2/z3_new_proof.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Fri Mar 21 20:39:54 2014 +0100 @@ -463,7 +463,7 @@ val match = Sign.typ_match (Proof_Context.theory_of ctxt) val t' = singleton (Variable.polymorphic ctxt) t - val patTs = map snd (Term.strip_qnt_vars @{const_name all} t') + val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t') val objTs = map (the o Symtab.lookup env) bounds val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty) in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end @@ -501,7 +501,7 @@ SOME (tyenv, _) => subst_of tyenv | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj)) -fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) = +fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) = dest_all (i + 1) (Term.betapply (a, Var (("", i), T))) | dest_all i t = (i, t) @@ -517,7 +517,7 @@ | SOME subst => let val applyT = Same.commit (substTs_same subst) - val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'') + val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'') in SOME (Symtab.make (bs' ~~ map applyT patTs)) end) end diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/SMT2/z3_new_replay.ML --- a/src/HOL/Tools/SMT2/z3_new_replay.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Fri Mar 21 20:39:54 2014 +0100 @@ -14,7 +14,7 @@ structure Z3_New_Replay: Z3_NEW_REPLAY = struct -fun params_of t = Term.strip_qnt_vars @{const_name all} t +fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t fun varify ctxt thm = let @@ -32,7 +32,7 @@ fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T))) in (ctxt', Symtab.make (map2 mk nTs ns)) end -fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) = +fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) = Term.betapply (a, Thm.term_of ct) | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt]) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 21 20:39:54 2014 +0100 @@ -85,8 +85,8 @@ fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t - | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2 - | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 + | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2 + | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def _ = false @@ -260,13 +260,13 @@ else Interesting fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t - | interest_of_prop Ts (@{const "==>"} $ t $ u) = + | interest_of_prop Ts (@{const Pure.imp} $ t $ u) = combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) - | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) = + | interest_of_prop Ts (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t - | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) = + | interest_of_prop Ts ((t as Const (@{const_name Pure.all}, _)) $ u) = interest_of_prop Ts (t $ eta_expand Ts u 1) - | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) = + | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) = combine_interests (interest_of_bool t) (interest_of_bool u) | interest_of_prop _ _ = Deal_Breaker val t = prop_of th @@ -351,7 +351,7 @@ | normalize_eq (@{const Trueprop} $ (t as @{const Not} $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1) - | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) = + | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) = (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1)) |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2) | normalize_eq t = t diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Mar 21 20:39:54 2014 +0100 @@ -187,9 +187,9 @@ if T = HOLogic.boolT then do_formula else do_term ext_arg and do_formula t = (case t of - Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t' - | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2 - | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => + Const (@{const_name Pure.all}, _) $ Abs (_, _, t') => do_formula t' + | @{const Pure.imp} $ t1 $ t2 => do_formula t1 #> do_formula t2 + | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 => do_term_or_formula false T t1 #> do_term_or_formula true T t2 | @{const Trueprop} $ t1 => do_formula t1 | @{const False} => I diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 21 20:39:54 2014 +0100 @@ -77,10 +77,10 @@ fun do_formula pos t = (case (pos, t) of (_, @{const Trueprop} $ t1) => do_formula pos t1 - | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t' + | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t' - | (_, @{const "==>"} $ t1 $ t2) => + | (_, @{const Pure.imp} $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2) | (_, @{const HOL.implies} $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2) @@ -88,7 +88,7 @@ | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 - | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 + | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/TFL/post.ML Fri Mar 21 20:39:54 2014 +0100 @@ -63,7 +63,7 @@ val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; fun mk_meta_eq r = case concl_of r of - Const("==",_)$_$_ => r + Const(@{const_name Pure.eq},_)$_$_ => r | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection | _ => r RS P_imp_P_eq_True diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/TFL/rules.ML Fri Mar 21 20:39:54 2014 +0100 @@ -293,7 +293,7 @@ fun GEN v th = let val gth = Thm.forall_intr v th val thy = Thm.theory_of_thm gth - val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth + val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); val allI2 = Drule.instantiate_normalize (certify thy theta) allI @@ -441,21 +441,22 @@ (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) fun is_cong thm = - case (Thm.prop_of thm) - of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $ - (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false - | _ => true; + case (Thm.prop_of thm) of + (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $ + (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => + false + | _ => true; -fun dest_equal(Const ("==",_) $ +fun dest_equal(Const (@{const_name Pure.eq},_) $ (Const (@{const_name Trueprop},_) $ lhs) $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs} - | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} + | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} | dest_equal tm = USyntax.dest_eq tm; fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); -fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a +fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; val is_all = can (dest_all []); @@ -468,10 +469,10 @@ end else ([], fm, used); -fun break_all(Const("all",_) $ Abs (_,_,body)) = body +fun break_all(Const(@{const_name Pure.all},_) $ Abs (_,_,body)) = body | break_all _ = raise RULES_ERR "break_all" "not a !!"; -fun list_break_all(Const("all",_) $ Abs (s,ty,body)) = +fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) = let val (L,core) = list_break_all body in ((s,ty)::L, core) end @@ -725,7 +726,7 @@ fun eliminate thm = case Thm.prop_of thm - of Const("==>",_) $ imp $ _ => + of Const(@{const_name Pure.imp},_) $ imp $ _ => eliminate (if not(is_all imp) then uq_eliminate (thm, imp, Thm.theory_of_thm thm) @@ -740,7 +741,8 @@ val cntxt = rev (Simplifier.prems_of ctxt) val dummy = print_thms ctxt "cntxt:" cntxt val thy = Thm.theory_of_thm thm - val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm + val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = + Thm.prop_of thm fun genl tm = let val vlist = subtract (op aconv) globals (Misc_Legacy.add_term_frees(tm,[])) in fold_rev Forall vlist tm diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/TFL/tfl.ML Fri Mar 21 20:39:54 2014 +0100 @@ -357,7 +357,7 @@ (*For Isabelle, the lhs of a definition must be a constant.*) fun const_def sign (c, Ty, rhs) = singleton (Syntax.check_terms (Proof_Context.init_global sign)) - (Const("==",dummyT) $ Const(c,Ty) $ rhs); + (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs); (*Make all TVars available for instantiation by adding a ? to the front*) fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/code_evaluation.ML Fri Mar 21 20:39:54 2014 +0100 @@ -193,7 +193,7 @@ val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); val t = Thm.term_of ct; val T = fastype_of t; - val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT))); + val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT))); in case value ctxt t of NONE => Thm.reflexive ct | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD} @@ -206,9 +206,9 @@ fun static_conv ctxt consts Ts = let - val eqs = "==" :: @{const_name HOL.eq} :: + val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} :: map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt) - (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*) + (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*) val value = static_value ctxt consts Ts; val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts); in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/inductive.ML Fri Mar 21 20:39:54 2014 +0100 @@ -258,7 +258,7 @@ handle THM _ => thm RS @{thm le_boolD} in (case concl_of thm of - Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) + Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Mar 21 20:39:54 2014 +0100 @@ -31,20 +31,21 @@ val pred_of = fst o dest_Const o head_of; -fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) = +fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) = let val (s', names') = (case names of [] => (singleton (Name.variant_list used) s, []) | name :: names' => (name, names')) in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end - | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) = + | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) = t $ strip_all' used names Q | strip_all' _ _ t = t; fun strip_all t = strip_all' (Term.add_free_names t []) [] t; -fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) = +fun strip_one name + (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) = (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q)) - | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q); + | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q); fun relevant_vars prop = fold (fn ((a, i), T) => fn vs => (case strip_type T of @@ -145,8 +146,8 @@ val is_rec = exists_Const (fn (c, _) => member (op =) rsets c); - fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P - | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q + fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P + | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q | is_meta (Const (@{const_name Trueprop}, _) $ t) = (case head_of t of Const (s, _) => can (Inductive.the_inductive ctxt) s diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/inductive_set.ML Fri Mar 21 20:39:54 2014 +0100 @@ -50,7 +50,7 @@ addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1 in SOME (Goal.prove ctxt [] [] - (Const ("==", T --> T --> propT) $ S $ S') + (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S') (K (EVERY [rtac eq_reflection 1, rtac @{thm subset_antisym} 1, rtac subsetI 1, dtac CollectD 1, simp, diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/record.ML Fri Mar 21 20:39:54 2014 +0100 @@ -1287,7 +1287,7 @@ (fn ctxt => fn t => (case t of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => - if quantifier = @{const_name all} orelse + if quantifier = @{const_name Pure.all} orelse quantifier = @{const_name All} orelse quantifier = @{const_name Ex} then @@ -1301,7 +1301,7 @@ | SOME (all_thm, All_thm, Ex_thm, _) => SOME (case quantifier of - @{const_name all} => all_thm + @{const_name Pure.all} => all_thm | @{const_name All} => All_thm RS @{thm eq_reflection} | @{const_name Ex} => Ex_thm RS @{thm eq_reflection} | _ => raise Fail "split_simproc")) @@ -1368,8 +1368,8 @@ val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso - is_recT T + (s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex}) + andalso is_recT T | _ => false); fun mk_split_free_tac free induct_thm i = @@ -1418,10 +1418,10 @@ val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T + (s = @{const_name Pure.all} orelse s = @{const_name All}) andalso is_recT T | _ => false); - fun is_all (Const (@{const_name all}, _) $ _) = ~1 + fun is_all (Const (@{const_name Pure.all}, _) $ _) = ~1 | is_all (Const (@{const_name All}, _) $ _) = ~1 | is_all _ = 0; in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Tools/simpdata.ML Fri Mar 21 20:39:54 2014 +0100 @@ -43,7 +43,7 @@ fun mk_eq th = case concl_of th (*expects Trueprop if not == *) - of Const (@{const_name "=="},_) $ _ $ _ => th + of Const (@{const_name Pure.eq},_) $ _ $ _ => th | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} | _ => th RS @{thm Eq_TrueI} diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/Typerep.thy Fri Mar 21 20:39:54 2014 +0100 @@ -24,7 +24,7 @@ let fun typerep_tr (*"_TYPEREP"*) [ty] = Syntax.const @{const_syntax typerep} $ - (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ + (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax Pure.type} $ (Syntax.const @{type_syntax itself} $ ty)) | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end @@ -34,7 +34,7 @@ let fun typerep_tr' ctxt (*"typerep"*) (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _])) - (Const (@{const_syntax TYPE}, _) :: ts) = + (Const (@{const_syntax Pure.type}, _) :: ts) = Term.list_comb (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts) | typerep_tr' _ T ts = raise Match; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/ex/Refute_Examples.thy Fri Mar 21 20:39:54 2014 +0100 @@ -325,7 +325,7 @@ refute [expect = genuine] oops -lemma "(x == all) \ False" +lemma "(x == Pure.all) \ False" refute [expect = genuine] oops diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/ex/SVC_Oracle.thy Fri Mar 21 20:39:54 2014 +0100 @@ -100,7 +100,7 @@ | fm t = replace t (*entry point, and abstraction of a meta-formula*) fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p) - | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) + | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) = c $ (mt p) $ (mt q) | mt t = fm t (*it might be a formula*) in (Logic.list_all (params, mt body), !pairs) end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/HOL/ex/svc_funcs.ML Fri Mar 21 20:39:54 2014 +0100 @@ -232,7 +232,7 @@ | fm pos t = var(t,[]); (*entry point, and translation of a meta-formula*) fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p) - | mt pos ((c as Const("==>", _)) $ p $ q) = + | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) = Buildin("=>", [mt (not pos) p, mt pos q]) | mt pos t = fm pos (iff_tag t) (*it might be a formula*) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Provers/blast.ML Fri Mar 21 20:39:54 2014 +0100 @@ -419,11 +419,12 @@ (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) -fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B +fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) = + strip_Trueprop A :: strip_imp_prems B | strip_imp_prems _ = []; (* A1==>...An==>B goes to B, where B is not an implication *) -fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B +fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B | strip_imp_concl A = strip_Trueprop A; @@ -443,7 +444,7 @@ else P :: delete_concl Ps | _ => P :: delete_concl Ps); -fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) = +fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) = skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P)) | skoPrem _ _ P = P; @@ -1177,7 +1178,7 @@ (*Make a list of all the parameters in a subgoal, even if nested*) local open Term in -fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t +fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t | discard_foralls t = t; end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Provers/hypsubst.ML Fri Mar 21 20:39:54 2014 +0100 @@ -104,8 +104,8 @@ (*Locates a substitutable variable on the left (resp. right) of an equality assumption. Returns the number of intervening assumptions. *) fun eq_var bnd novars = - let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t - | eq_var_aux k (Const("==>",_) $ A $ B) = + let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t + | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) = ((k, inspect_pair bnd novars (Data.dest_eq (Data.dest_Trueprop A))) handle TERM _ => eq_var_aux (k+1) B diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Provers/splitter.ML Fri Mar 21 20:39:54 2014 +0100 @@ -57,7 +57,7 @@ fun split_format_err () = error "Wrong format for split rule"; fun split_thm_info thm = case concl_of (Data.mk_eq thm) of - Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of + Const(@{const_name Pure.eq}, _) $ (Var _ $ t) $ c => (case strip_comb t of (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false) | _ => split_format_err ()) | _ => split_format_err (); @@ -393,9 +393,9 @@ fun tac (t,i) = let val n = find_index (exists_Const (member (op =) cname_list o #1)) (Logic.strip_assums_hyp t); - fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _) + fun first_prem_is_disj (Const (@{const_name Pure.imp}, _) $ (Const (c, _) $ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or - | first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = + | first_prem_is_disj (Const(@{const_name Pure.all},_)$Abs(_,_,t)) = first_prem_is_disj t | first_prem_is_disj _ = false; (* does not work properly if the split variable is bound by a quantifier *) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Isar/isar_syn.ML Fri Mar 21 20:39:54 2014 +0100 @@ -108,7 +108,7 @@ val _ = Outer_Syntax.command @{command_spec "consts"} "declare constants" - (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts)); + (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); val mode_spec = (@{keyword "output"} >> K ("", false)) || @@ -119,11 +119,13 @@ val _ = Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses" - (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax)); + (opt_mode -- Scan.repeat1 Parse.const_decl + >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses" - (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax)); + (opt_mode -- Scan.repeat1 Parse.const_decl + >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); (* translations *) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Isar/object_logic.ML Fri Mar 21 20:39:54 2014 +0100 @@ -97,8 +97,8 @@ in -val add_judgment = gen_add_judgment Sign.add_consts_i; -val add_judgment_cmd = gen_add_judgment Sign.add_consts; +val add_judgment = gen_add_judgment Sign.add_consts; +val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd; end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Proof/extraction.ML Fri Mar 21 20:39:54 2014 +0100 @@ -37,7 +37,7 @@ val add_syntax = Sign.root_path #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)] - #> Sign.add_consts_i + #> Sign.add_consts [(Binding.name "typeof", typ "'b => Type", NoSyn), (Binding.name "Type", typ "'a itself => Type", NoSyn), (Binding.name "Null", typ "Null", NoSyn), @@ -791,7 +791,7 @@ val fu = Type.legacy_freeze u; val (def_thms, thy') = if t = nullt then ([], thy) else thy - |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)] + |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)] |> Global_Theory.add_defs false [((Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 21 20:39:54 2014 +0100 @@ -48,14 +48,14 @@ SOME (equal_intr_axm % B % A %% prf2 %% prf1) | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) % + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) % + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %% ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% @@ -63,7 +63,7 @@ | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) = let val _ $ A $ C = Envir.beta_norm X; @@ -78,7 +78,7 @@ | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) = let val _ $ A $ C = Envir.beta_norm Y; @@ -91,7 +91,7 @@ end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) = let @@ -104,7 +104,7 @@ | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) = let @@ -140,7 +140,7 @@ | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %% (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) = SOME (equal_elim_axm %> C %> D %% prf2 %% (equal_elim_axm %> A %> C %% prf3 %% @@ -150,7 +150,7 @@ (PAxm ("Pure.symmetric", _, _) % _ % _ %% (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) = SOME (equal_elim_axm %> A %> B %% prf1 %% (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %% @@ -160,7 +160,7 @@ (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) = SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% (equal_elim_axm %> B %> D %% prf3 %% @@ -171,14 +171,14 @@ (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %% - (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %% + (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) = SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %% (equal_elim_axm %> C %> D %% prf2 %% prf4))) | rew' ((prf as PAxm ("Pure.combination", _, _) % - SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %% + SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %% (PAxm ("Pure.reflexive", _, _) % _)) = let val (U, V) = (case T of Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT)) @@ -307,9 +307,9 @@ val Hs' = Logic.strip_assums_hyp Q; val k = length Hs; val l = length params; - fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf = + fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf = mk_prf i (j - 1) Hs Hs' P (prf %> Bound j) - | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf = + | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf = mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i)) | mk_prf _ _ _ _ _ prf = prf in @@ -324,9 +324,9 @@ val Hs' = Logic.strip_assums_hyp Q; val k = length Hs; val l = length params; - fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf = + fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf = Abst (s, SOME T, mk_prf P prf) - | mk_prf (Const ("==>", _) $ P $ Q) prf = + | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf = AbsP ("H", SOME P, mk_prf Q prf) | mk_prf _ prf = prf in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 20:39:54 2014 +0100 @@ -35,7 +35,7 @@ fun add_proof_atom_consts names thy = thy |> Sign.root_path - |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); + |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); (** constants for application and abstraction **) @@ -54,7 +54,7 @@ ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn), ((Binding.name "MinProof", proofT), Delimfix "?")] |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"] - |> Sign.add_syntax_i + |> Sign.add_syntax Syntax.mode_default [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), @@ -62,7 +62,7 @@ ("", paramT --> paramT, Delimfix "'(_')"), ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] - |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) + |> Sign.add_syntax (Symbol.xsymbolsN, true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] @@ -127,16 +127,16 @@ Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = AbsP (s, case t of - Const ("dummy_pattern", _) => NONE - | _ $ Const ("dummy_pattern", _) => NONE + Const ("Pure.dummy_pattern", _) => NONE + | _ $ Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t), Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = prf_of [] prf1 %% prf_of [] prf2 - | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = + | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = prf_of (T::Ts) prf | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % - (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) + (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) | prf_of _ t = error ("Not a proof term:\n" ^ Syntax.string_of_term_global thy t) diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Proof/reconstruct.ML Fri Mar 21 20:39:54 2014 +0100 @@ -155,7 +155,7 @@ | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; - in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), + in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = @@ -173,7 +173,7 @@ | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of - (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => + (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) env'' vTs'' (u, u') | (t, prf1, cnstrts', env'', vTs'') => @@ -185,7 +185,7 @@ | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of - (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, + (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env2, vTs2) => let val env3 = unifyT thy env2 T U in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) @@ -194,12 +194,12 @@ let val (v, env3) = mk_var env2 Ts (U --> propT); in add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 - (u, Const ("all", (U --> propT) --> propT) $ v) + (u, Const ("Pure.all", (U --> propT) --> propT) $ v) end) end | mk_cnstrts env Ts Hs vTs (cprf % NONE) = (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of - (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, + (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env', vTs') => let val (t, env'') = mk_var env' Ts T in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') @@ -211,7 +211,7 @@ val (t, env3) = mk_var env2 Ts T in add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' - (u, Const ("all", (T --> propT) --> propT) $ v) + (u, Const ("Pure.all", (T --> propT) --> propT) $ v) end) | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) = mk_cnstrts_atom env vTs prop opTs prf @@ -309,10 +309,10 @@ | prop_of0 Hs (AbsP (s, SOME t, prf)) = Logic.mk_implies (t, prop_of0 (t :: Hs) prf) | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of - Const ("all", _) $ f => f $ t + Const ("Pure.all", _) $ f => f $ t | _ => error "prop_of: all expected") | prop_of0 Hs (prf1 %% prf2) = (case head_norm (prop_of0 Hs prf1) of - Const ("==>", _) $ P $ Q => Q + Const ("Pure.imp", _) $ P $ Q => Q | _ => error "prop_of: ==> expected") | prop_of0 Hs (Hyp t) = t | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Syntax/simple_syntax.ML --- a/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 20:39:54 2014 +0100 @@ -107,12 +107,12 @@ (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies || term2 env T) x and term2 env T x = - (equal env "==" || + (equal env || term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction || term3 env T) x -and equal env eq x = - (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) => - Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x +and equal env x = + (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) => + Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x and term3 env T x = (idt >> Free || var -- constraint >> Var || diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 20:39:54 2014 +0100 @@ -177,7 +177,7 @@ in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok - | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) = + | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) = [ast_of_dummy a tok] | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) = [ast_of_dummy a tok] @@ -568,7 +568,7 @@ | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t) - | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = + | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) = if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1 else mark Ts t1 $ mark Ts t2 | mark Ts (t as t1 $ t2) = @@ -834,7 +834,7 @@ ("_context_xconst", const_ast_tr false)] #> Sign.typed_print_translation [("_type_prop", type_prop_tr'), - ("\\<^const>TYPE", type_tr'), + ("\\<^const>Pure.type", type_tr'), ("_type_constraint_", type_constraint_tr')]); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 20:39:54 2014 +0100 @@ -152,7 +152,7 @@ fun mk_type ty = Syntax.const "_constrain" $ - Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); + Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty); fun ofclass_tr [ty, cls] = cls $ mk_type ty | ofclass_tr ts = raise TERM ("ofclass_tr", ts); @@ -174,7 +174,7 @@ (case Ast.unfold_ast_p "_asms" asms of (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] | _ => raise Ast.AST ("bigimpl_ast_tr", asts)) - in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end + in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts); @@ -382,7 +382,8 @@ fun impl_ast_tr' asts = if no_brackets () then raise Match else - (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of + (case Ast.unfold_ast_p "\\<^const>Pure.imp" + (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of (prems as _ :: _ :: _, concl) => let val (asms, asm) = split_last prems; @@ -498,7 +499,7 @@ ("_abs", fn _ => abs_ast_tr'), ("_idts", fn _ => idtyp_ast_tr' "_idts"), ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"), - ("\\<^const>==>", fn _ => impl_ast_tr'), + ("\\<^const>Pure.imp", fn _ => impl_ast_tr'), ("_index", fn _ => index_ast_tr')]; end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/conv.ML --- a/src/Pure/conv.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/conv.ML Fri Mar 21 20:39:54 2014 +0100 @@ -140,17 +140,17 @@ fun forall_conv cv ctxt ct = (case Thm.term_of ct of - Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct + Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct | _ => raise CTERM ("forall_conv", [ct])); fun implies_conv cv1 cv2 ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct + Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct | _ => raise CTERM ("implies_conv", [ct])); fun implies_concl_conv cv ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => arg_conv cv ct + Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct | _ => raise CTERM ("implies_concl_conv", [ct])); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/drule.ML Fri Mar 21 20:39:54 2014 +0100 @@ -126,7 +126,7 @@ (* A1==>...An==>B goes to B, where B is not an implication *) fun strip_imp_concl ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) + Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) | _ => ct); (*The premises of a theorem, as a cterm list*) @@ -706,7 +706,7 @@ val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false - | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false + | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false | is_norm_hhf (Abs _ $ _) = false | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/goal.ML Fri Mar 21 20:39:54 2014 +0100 @@ -327,8 +327,8 @@ (* non-atomic goal assumptions *) -fun non_atomic (Const ("==>", _) $ _ $ _) = true - | non_atomic (Const ("all", _) $ _) = true +fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true + | non_atomic (Const ("Pure.all", _) $ _) = true | non_atomic _ = false; fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/logic.ML Fri Mar 21 20:39:54 2014 +0100 @@ -93,14 +93,14 @@ (** all **) -fun all_const T = Const ("all", (T --> propT) --> propT); +fun all_const T = Const ("Pure.all", (T --> propT) --> propT); fun all v t = all_const (Term.fastype_of v) $ lambda v t; -fun is_all (Const ("all", _) $ Abs _) = true +fun is_all (Const ("Pure.all", _) $ Abs _) = true | is_all _ = false; -fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) = +fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) = let val (x, b) = Term.dest_abs abs (*potentially slow*) in ((x, T), b) end | dest_all t = raise TERM ("dest_all", [t]); @@ -113,19 +113,19 @@ fun mk_equals (t, u) = let val T = Term.fastype_of t - in Const ("==", T --> T --> propT) $ t $ u end; + in Const ("Pure.eq", T --> T --> propT) $ t $ u end; -fun dest_equals (Const ("==", _) $ t $ u) = (t, u) +fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u) | dest_equals t = raise TERM ("dest_equals", [t]); (** implies **) -val implies = Const ("==>", propT --> propT --> propT); +val implies = Const ("Pure.imp", propT --> propT --> propT); fun mk_implies (A, B) = implies $ A $ B; -fun dest_implies (Const ("==>", _) $ A $ B) = (A, B) +fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B) | dest_implies A = raise TERM ("dest_implies", [A]); @@ -136,28 +136,28 @@ | list_implies (A::As, B) = implies $ A $ list_implies(As,B); (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) -fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B +fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B | strip_imp_prems _ = []; (* A1==>...An==>B goes to B, where B is not an implication *) -fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B +fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B | strip_imp_concl A = A : term; (*Strip and return premises: (i, [], A1==>...Ai==>B) goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) if i<0 or else i too big then raises TERM*) fun strip_prems (0, As, B) = (As, B) - | strip_prems (i, As, Const("==>", _) $ A $ B) = + | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) = strip_prems (i-1, A::As, B) | strip_prems (_, As, A) = raise TERM("strip_prems", A::As); (*Count premises -- quicker than (length o strip_prems) *) -fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B +fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B | count_prems _ = 0; (*Select Ai from A1 ==>...Ai==>B*) -fun nth_prem (1, Const ("==>", _) $ A $ _) = A - | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B) +fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A + | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B) | nth_prem (_, A) = raise TERM ("nth_prem", [A]); (*strip a proof state (Horn clause): @@ -208,9 +208,9 @@ (** types as terms **) -fun mk_type ty = Const ("TYPE", Term.itselfT ty); +fun mk_type ty = Const ("Pure.type", Term.itselfT ty); -fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty +fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty | dest_type t = raise TERM ("dest_type", [t]); fun type_map f = dest_type o f o mk_type; @@ -323,10 +323,10 @@ (** protected propositions and embedded terms **) -val protectC = Const ("prop", propT --> propT); +val protectC = Const ("Pure.prop", propT --> propT); fun protect t = protectC $ t; -fun unprotect (Const ("prop", _) $ t) = t +fun unprotect (Const ("Pure.prop", _) $ t) = t | unprotect t = raise TERM ("unprotect", [t]); @@ -395,46 +395,46 @@ fun lift_abs inc = let - fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t - | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) + fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t + | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) | lift Ts _ t = incr_indexes (rev Ts, inc) t; in lift [] end; fun lift_all inc = let - fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t - | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) + fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t + | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) | lift Ts _ t = incr_indexes (rev Ts, inc) t; in lift [] end; (*Strips assumptions in goal, yielding list of hypotheses. *) fun strip_assums_hyp B = let - fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B - | strip Hs (Const ("all", _) $ Abs (a, T, t)) = + fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B + | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) = strip (map (incr_boundvars 1) Hs) t | strip Hs B = rev Hs in strip [] B end; (*Strips assumptions in goal, yielding conclusion. *) -fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B - | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t +fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B + | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t | strip_assums_concl B = B; (*Make a list of all the parameters in a subgoal, even if nested*) -fun strip_params (Const("==>", _) $ H $ B) = strip_params B - | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t +fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B + | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t | strip_params B = []; (*test for nested meta connectives in prems*) val has_meta_prems = let - fun is_meta (Const ("==", _) $ _ $ _) = true - | is_meta (Const ("==>", _) $ _ $ _) = true - | is_meta (Const ("all", _) $ _) = true + fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true + | is_meta (Const ("Pure.imp", _) $ _ $ _) = true + | is_meta (Const ("Pure.all", _) $ _) = true | is_meta _ = false; - fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B - | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B + fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B + | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B | ex_meta _ = false; in ex_meta end; @@ -444,10 +444,10 @@ fun remove_params j n A = if j=0 andalso n<=0 then A (*nothing left to do...*) else case A of - Const("==>", _) $ H $ B => + Const("Pure.imp", _) $ H $ B => if n=1 then (remove_params j (n-1) B) else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) - | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t + | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t | _ => if n>0 then raise TERM("remove_params", [A]) else A; @@ -460,9 +460,9 @@ in list_all (vars, remove_params (length vars) n A) end; (*Makes parameters in a goal have the names supplied by the list cs.*) -fun list_rename_params cs (Const ("==>", _) $ A $ B) = +fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) = implies $ A $ list_rename_params cs B - | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) = + | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) = a $ Abs (c, T, list_rename_params cs t) | list_rename_params cs B = B; @@ -480,12 +480,12 @@ Unless nasms<0, it can terminate the recursion early; that allows erule to work on assumptions of the form P==>Q.*) fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) - | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = + | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) = strip_assums_imp (nasms-1, H::Hs, B) | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) (*Strips OUTER parameters only.*) -fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) = +fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_all ((a,T)::params, t) | strip_assums_all (params, B) = (params, B); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/more_thm.ML Fri Mar 21 20:39:54 2014 +0100 @@ -127,7 +127,7 @@ let val cert = Thm.cterm_of (Thm.theory_of_cterm t); val T = #T (Thm.rep_cterm t); - in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end; + in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end; fun all t A = all_name ("", t) A; @@ -136,22 +136,22 @@ fun dest_implies ct = (case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => dest_binop ct + Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of - Const ("==", _) $ _ $ _ => dest_binop ct + Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of - Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct + Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of - Const ("==", _) $ _ $ _ => Thm.dest_arg ct + Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; @@ -337,7 +337,7 @@ fun forall_elim_var i th = forall_elim_vars_aux - (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)] + (fn Const ("Pure.all", _) $ Abs (a, T, _) => [(a, T)] | _ => raise THM ("forall_elim_vars", i, [th])) i th; end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/primitive_defs.ML Fri Mar 21 20:39:54 2014 +0100 @@ -37,7 +37,7 @@ fun check_arg (Bound _) = true | check_arg (Free (x, _)) = not (is_fixed x) - | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true + | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true | check_arg _ = false; fun close_arg (Bound _) t = t | close_arg x t = Logic.all x t; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/proofterm.ML Fri Mar 21 20:39:54 2014 +0100 @@ -865,9 +865,9 @@ fun mk_app b (i, j, prf) = if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); - fun lift Us bs i j (Const ("==>", _) $ A $ B) = + fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) = AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) - | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = + | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k)))) @@ -886,9 +886,9 @@ fun mk_asm_prf t i m = let fun imp_prf _ i 0 = PBound i - | imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1)) + | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1)) | imp_prf _ i _ = PBound i; - fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) + fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) | all_prf t = imp_prf t (~i) m in all_prf t end; @@ -899,9 +899,9 @@ (***** Composition of object rule with proof state *****) -fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) = +fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) = AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) - | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) = + | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) = Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0))); @@ -1091,9 +1091,9 @@ if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; -fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) = +fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) = add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) - | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) = + | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) = add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) @@ -1105,8 +1105,8 @@ | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); -fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) - | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t +fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) + | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); @@ -1196,7 +1196,7 @@ (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) | (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end - and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = + and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) = union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) | needed (Var (ixn, _)) (_::_) _ = [ixn] | needed _ _ _ = []; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/pure_thy.ML Fri Mar 21 20:39:54 2014 +0100 @@ -49,8 +49,8 @@ val old_appl_syntax_setup = Old_Appl_Syntax.put true #> - Sign.del_modesyntax_i Syntax.mode_default applC_syntax #> - Sign.add_syntax_i appl_syntax; + Sign.del_syntax Syntax.mode_default applC_syntax #> + Sign.add_syntax Syntax.mode_default appl_syntax; (* main content *) @@ -75,8 +75,8 @@ "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) - #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers) - #> Sign.add_syntax_i + #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) + #> Sign.add_syntax Syntax.mode_default [("", typ "prop' => prop", Delimfix "_"), ("", typ "logic => any", Delimfix "_"), ("", typ "prop' => any", Delimfix "_"), @@ -169,13 +169,13 @@ ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"), ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"), ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"), - (const "==>", typ "prop => prop => prop", Delimfix "op ==>"), - (const "dummy_pattern", typ "aprop", Delimfix "'_"), + (const "Pure.imp", typ "prop => prop => prop", Delimfix "op ==>"), + (const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] - #> Sign.add_syntax_i applC_syntax - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) + #> Sign.add_syntax Syntax.mode_default applC_syntax + #> Sign.add_syntax (Symbol.xsymbolsN, true) [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), @@ -184,42 +184,42 @@ ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - (const "==", typ "'a => 'a => prop", Infix ("\\", 2)), - (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), + (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\", 2)), + (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\", 1)), ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] - #> Sign.add_modesyntax_i ("", false) - [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))] - #> Sign.add_modesyntax_i ("HTML", false) + #> Sign.add_syntax ("", false) + [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))] + #> Sign.add_syntax ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] - #> Sign.add_consts_i - [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)), - (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), - (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), - (Binding.name "prop", typ "prop => prop", NoSyn), - (Binding.name "TYPE", typ "'a itself", NoSyn), - (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")] - #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] - #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] - #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] - #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] - #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") [] + #> Sign.add_consts + [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)), + (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), + (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)), + (qualify (Binding.name "prop"), typ "prop => prop", NoSyn), + (qualify (Binding.name "type"), typ "'a itself", NoSyn), + (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")] + #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") [] + #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") [] + #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") [] + #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") [] + #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") [] #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation - #> Sign.add_consts_i + #> Sign.add_consts [(qualify (Binding.name "term"), typ "'a => prop", NoSyn), (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn), (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)] #> Sign.local_path #> (Global_Theory.add_defs false o map Thm.no_attributes) - [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), + [(Binding.name "prop_def", prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"), (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), (Binding.name "sort_constraint_def", - prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\ - \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"), + prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\ + \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"), (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd #> fold (fn (a, prop) => diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/raw_simplifier.ML Fri Mar 21 20:39:54 2014 +0100 @@ -599,7 +599,7 @@ | is_full_cong_prems [] _ = false | is_full_cong_prems (p :: prems) varpairs = (case Logic.strip_assums_concl p of - Const ("==", _) $ lhs $ rhs => + Const ("Pure.eq", _) $ lhs $ rhs => let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in is_Var x andalso forall is_Bound xs andalso not (has_duplicates (op =) xs) andalso xs = ys andalso @@ -981,7 +981,7 @@ let fun is_simple ({thm, ...}: rrule) = (case Thm.prop_of thm of - Const ("==", _) $ _ $ _ => true + Const ("Pure.eq", _) $ _ $ _ => true | _ => false); fun sort [] (re1, re2) = re1 @ re2 | sort (rr :: rrs) (re1, re2) = @@ -1099,7 +1099,7 @@ end | t $ _ => (case t of - Const ("==>", _) $ _ => impc t0 ctxt + Const ("Pure.imp", _) $ _ => impc t0 ctxt | Abs _ => let val thm = Thm.beta_conversion false t0 in diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/sign.ML Fri Mar 21 20:39:54 2014 +0100 @@ -73,18 +73,16 @@ val add_nonterminals: Proof.context -> binding list -> theory -> theory val add_nonterminals_global: binding list -> theory -> theory val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory - val add_syntax: (string * string * mixfix) list -> theory -> theory - val add_syntax_i: (string * typ * mixfix) list -> theory -> theory - val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory - val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory - val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory - val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory + val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory + val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory + val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory + val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory - val add_consts: (binding * string * mixfix) list -> theory -> theory - val add_consts_i: (binding * typ * mixfix) list -> theory -> theory + val add_consts: (binding * typ * mixfix) list -> theory -> theory + val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory val add_abbrev: string -> binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory @@ -375,12 +373,10 @@ fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x; -val add_modesyntax = gen_add_syntax Syntax.read_typ; -val add_modesyntax_i = gen_add_syntax (K I); -val add_syntax = add_modesyntax Syntax.mode_default; -val add_syntax_i = add_modesyntax_i Syntax.mode_default; -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ; -val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I); +val add_syntax = gen_add_syntax (K I); +val add_syntax_cmd = gen_add_syntax Syntax.read_typ; +val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I); +val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ; fun type_notation add mode args = let @@ -417,17 +413,17 @@ in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) - |> add_syntax_i (map #2 args) + |> add_syntax Syntax.mode_default (map #2 args) |> pair (map #3 args) end; in fun add_consts args thy = - #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); + #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy); -fun add_consts_i args thy = - #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy); +fun add_consts_cmd args thy = + #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx); fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy; @@ -468,7 +464,7 @@ |> map_sign (fn (syn, tsig, consts) => let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig; in (syn, tsig', consts) end) - |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; + |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/term.ML --- a/src/Pure/term.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/term.ML Fri Mar 21 20:39:54 2014 +0100 @@ -579,11 +579,11 @@ val propT : typ = Type ("prop",[]); (* maps !!x1...xn. t to t *) -fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t +fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t)) = strip_all_body t | strip_all_body t = t; (* maps !!x1...xn. t to [x1, ..., xn] *) -fun strip_all_vars (Const("all",_)$Abs(a,T,t)) = +fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_all_vars t | strip_all_vars t = [] : (string*typ) list; @@ -816,7 +816,7 @@ fun close_schematic_term t = let - val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t); + val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t); val extra_terms = map Var (add_vars t []); in fold lambda (extra_terms @ extra_types) t end; @@ -924,18 +924,18 @@ (* dummy patterns *) -fun dummy_pattern T = Const ("dummy_pattern", T); +fun dummy_pattern T = Const ("Pure.dummy_pattern", T); val dummy = dummy_pattern dummyT; val dummy_prop = dummy_pattern propT; -fun is_dummy_pattern (Const ("dummy_pattern", _)) = true +fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true | is_dummy_pattern _ = false; fun no_dummy_patterns tm = if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); -fun free_dummy_patterns (Const ("dummy_pattern", T)) used = +fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used = let val [x] = Name.invent used Name.uu 1 in (Free (Name.internal x, T), Name.declare x used) end | free_dummy_patterns (Abs (x, T, b)) used = @@ -948,7 +948,7 @@ in (t' $ u', used'') end | free_dummy_patterns a used = (a, used); -fun replace_dummy Ts (Const ("dummy_pattern", T)) i = +fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i = (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_dummy Ts (Abs (x, T, t)) i = let val (t', i') = replace_dummy (T :: Ts) t i diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Pure/thm.ML Fri Mar 21 20:39:54 2014 +0100 @@ -687,7 +687,7 @@ fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); in case prop of - Const ("==>", _) $ A $ B => + Const ("Pure.imp", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, {thy = merge_thys2 thAB thA, @@ -741,7 +741,7 @@ (ct as Cterm {t, T, maxidx = maxt, sorts, ...}) (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of - Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => + Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else @@ -778,7 +778,7 @@ *) fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of - (eq as Const ("==", _)) $ t $ u => + (eq as Const ("Pure.eq", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric der, {thy = thy, tags = [], @@ -803,7 +803,7 @@ fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); in case (prop1, prop2) of - ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) => + ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, @@ -911,8 +911,8 @@ | _ => raise THM ("combination: not function type", 0, [th1, th2])); in (case (prop1, prop2) of - (Const ("==", Type ("fun", [fT, _])) $ f $ g, - Const ("==", Type ("fun", [tT, _])) $ t $ u) => + (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, + Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, {thy = merge_thys2 th1 th2, @@ -939,7 +939,7 @@ fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in (case (prop1, prop2) of - (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => + (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, {thy = merge_thys2 th1 th2, @@ -967,7 +967,7 @@ fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in (case prop1 of - Const ("==", _) $ A $ B => + Const ("Pure.eq", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, {thy = merge_thys2 th1 th2, @@ -1472,17 +1472,17 @@ (* strip_apply f B A strips off all assumptions/parameters from A introduced by lifting over B, and applies f to remaining part of A*) fun strip_apply f = - let fun strip (Const ("==>", _) $ _ $ B1) - (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) - | strip ((c as Const ("all", _)) $ Abs (_, _, t1)) - ( Const ("all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) + let fun strip (Const ("Pure.imp", _) $ _ $ B1) + (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) + | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1)) + ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) | strip _ A = f A in strip end; -fun strip_lifted (Const ("==>", _) $ _ $ B1) - (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2 - | strip_lifted (Const ("all", _) $ Abs (_, _, t1)) - (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 +fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1) + (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2 + | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1)) + (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 | strip_lifted _ A = A; (*Use the alist to rename all bound variables and some unknowns in a term @@ -1532,10 +1532,10 @@ (*strip off pairs of assumptions/parameters in parallel -- they are identical because of lifting*) -fun strip_assums2 (Const("==>", _) $ _ $ B1, - Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) - | strip_assums2 (Const("all",_)$Abs(a,T,t1), - Const("all",_)$Abs(_,_,t2)) = +fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1, + Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2) + | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1), + Const("Pure.all",_)$Abs(_,_,t2)) = let val (B1,B2) = strip_assums2 (t1,t2) in (Abs(a,T,B1), Abs(a,T,B2)) end | strip_assums2 BB = BB; @@ -1543,13 +1543,13 @@ (*Faster normalization: skip assumptions that were lifted over*) fun norm_term_skip env 0 t = Envir.norm_term env t - | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) = + | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = let val T' = Envir.subst_type (Envir.type_env env) T (*Must instantiate types of parameters because they are flattened; this could be a NEW parameter*) in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end - | norm_term_skip env n (Const ("==>", _) $ A $ B) = + | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = Logic.mk_implies (A, norm_term_skip env (n - 1) B) | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Sequents/simpdata.ML Fri Mar 21 20:39:54 2014 +0100 @@ -29,7 +29,7 @@ (*Make meta-equalities.*) fun mk_meta_eq ctxt th = case concl_of th of - Const("==",_)$_$_ => th + Const(@{const_name Pure.eq},_)$_$_ => th | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of ([], [p]) => diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/Code/code_runtime.ML Fri Mar 21 20:39:54 2014 +0100 @@ -163,7 +163,7 @@ val _ = if fastype_of t <> propT then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) else (); - val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); + val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t []) of SOME Holds => true | _ => false; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/Code/code_symbol.ML Fri Mar 21 20:39:54 2014 +0100 @@ -88,8 +88,8 @@ in fun default_base (Constant "") = "value" - | default_base (Constant "==>") = "follows" - | default_base (Constant "==") = "meta_eq" + | default_base (Constant @{const_name Pure.imp}) = "follows" + | default_base (Constant @{const_name Pure.eq}) = "meta_eq" | default_base (Constant c) = base c | default_base (Type_Constructor tyco) = base tyco | default_base (Type_Class class) = base class diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/Code/code_thingol.ML Fri Mar 21 20:39:54 2014 +0100 @@ -800,8 +800,8 @@ val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; - val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t; - val dummy_constant = Constant @{const_name dummy_pattern}; + val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t; + val dummy_constant = Constant @{const_name Pure.dummy_pattern}; val stmt_value = fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs ##>> translate_typ ctxt algbr eqngr false ty @@ -818,7 +818,7 @@ val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps, program2)) end; in - ensure_stmt Constant stmt_value @{const_name dummy_pattern} + ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern} #> snd #> term_value end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/induct.ML Fri Mar 21 20:39:54 2014 +0100 @@ -162,7 +162,7 @@ | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); val rearrange_eqs_simproc = - Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"] + Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"] (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t)); @@ -644,14 +644,16 @@ local -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) +fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) = + c $ Abs (a, T, goal_prefix k B) | goal_prefix 0 _ = Term.dummy_prop - | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B + | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) = + c $ A $ goal_prefix (k - 1) B | goal_prefix _ _ = Term.dummy_prop; -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 +fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1 | goal_params 0 _ = 0 - | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B + | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B | goal_params _ _ = 0; fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => @@ -670,11 +672,13 @@ [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); - fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B + fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) = + goal_concl k ((a, T) :: xs) B | goal_concl 0 xs B = if not (Term.exists_subterm (fn t => t aconv v) B) then NONE else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B)) - | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B + | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) = + goal_concl (k - 1) xs B | goal_concl _ _ _ = NONE; in (case goal_concl n [] goal of diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/misc_legacy.ML Fri Mar 21 20:39:54 2014 +0100 @@ -130,9 +130,9 @@ H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. Main difference from strip_assums concerns parameters: it replaces the bound variables by free variables. *) -fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) = +fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) = strip_context_aux (params, H :: Hs, B) - | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) = + | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) = let val (b, u) = Syntax_Trans.variant_abs (a, T, t) in strip_context_aux ((b, T) :: params, Hs, u) end | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/nbe.ML Fri Mar 21 20:39:54 2014 +0100 @@ -586,7 +586,7 @@ let val thy = Proof_Context.theory_of ctxt; val ty = Thm.typ_of (Thm.ctyp_of_term lhs); - val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT)); + val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT)); val rhs = Thm.cterm_of thy raw_rhs; in Thm.mk_binop eq lhs rhs end; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/Tools/quickcheck.ML Fri Mar 21 20:39:54 2014 +0100 @@ -358,7 +358,7 @@ val lthy = Proof.context_of state; val thy = Proof.theory_of state; val _ = message lthy "Quickchecking..." - fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t + fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t | strip t = t; val {goal = st, ...} = Proof.raw_goal state; val (gi, frees) = Logic.goal_params (prop_of st) i; diff -r 5d147e1e18d1 -r 2b2bcf4ecb48 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Mar 21 15:36:00 2014 +0000 +++ b/src/ZF/Tools/datatype_package.ML Fri Mar 21 20:39:54 2014 +0100 @@ -244,21 +244,20 @@ fun add_recursor thy = if need_recursor then thy - |> Sign.add_consts_i - [(Binding.name recursor_base_name, recursor_typ, NoSyn)] + |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)] |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) else thy; val (con_defs, thy0) = thy_path - |> Sign.add_consts_i - (map (fn (c, T, mx) => (Binding.name c, T, mx)) - ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) - |> Global_Theory.add_defs false - (map (Thm.no_attributes o apfst Binding.name) - (case_def :: - flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) - ||> add_recursor - ||> Sign.parent_path + |> Sign.add_consts + (map (fn (c, T, mx) => (Binding.name c, T, mx)) + ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) + |> Global_Theory.add_defs false + (map (Thm.no_attributes o apfst Binding.name) + (case_def :: + flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) + ||> add_recursor + ||> Sign.parent_path; val intr_names = map (Binding.name o #2) (flat con_ty_lists); val (thy1, ind_result) =