--- a/src/Doc/IsarImplementation/Logic.thy Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy Fri Mar 21 12:34:50 2014 +0100
@@ -850,7 +850,7 @@
@{text "#A \<equiv> A"} \\[1ex]
@{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
@{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
- @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
+ @{text "type :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
@{text "(unspecified)"} \\
\end{tabular}
\caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 21 12:34:50 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])
--- a/src/HOL/Library/Countable.thy Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Library/Countable.thy Fri Mar 21 12:34:50 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)
--- a/src/HOL/Library/refute.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Library/refute.ML Fri Mar 21 12:34:50 2014 +0100
@@ -548,7 +548,7 @@
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.type}, _) => t (* axiomatic type classes *)
(* HOL *)
| Const (@{const_name Trueprop}, _) => t
| Const (@{const_name Not}, _) => t
@@ -713,7 +713,7 @@
| Const (@{const_name "=="}, _) => axs
| Const (@{const_name "==>"}, _) => 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
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 12:34:50 2014 +0100
@@ -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
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 12:34:50 2014 +0100
@@ -437,7 +437,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])
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 12:34:50 2014 +0100
@@ -1444,7 +1444,7 @@
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
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 12:34:50 2014 +0100
@@ -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 _ =>
--- a/src/HOL/Typerep.thy Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Typerep.thy Fri Mar 21 12:34:50 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;
--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 12:34:50 2014 +0100
@@ -133,7 +133,7 @@
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 ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
--- a/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 12:34:50 2014 +0100
@@ -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')]);
--- a/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 12:34:50 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);
--- a/src/Pure/logic.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/logic.ML Fri Mar 21 12:34:50 2014 +0100
@@ -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;
--- a/src/Pure/primitive_defs.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/primitive_defs.ML Fri Mar 21 12:34:50 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;
--- a/src/Pure/pure_thy.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/pure_thy.ML Fri Mar 21 12:34:50 2014 +0100
@@ -199,12 +199,12 @@
(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),
+ (qualify (Binding.name "type"), typ "'a itself", NoSyn),
(qualify (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 "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
@@ -218,8 +218,8 @@
[(Binding.name "prop_def", prop "(CONST 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) =>
--- a/src/Pure/term.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/term.ML Fri Mar 21 12:34:50 2014 +0100
@@ -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;