# HG changeset patch
# User wenzelm
# Date 1395401690 -3600
# Node ID 2e10a36b8d46e81fb70731c28b59f546089abf33
# Parent  d0a9100a5a38287092cc96e24c0d0832cc9bd9e0
more qualified names;

diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Doc/IsarImplementation/Logic.thy
--- 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}
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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])
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Library/Countable.thy
--- 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)
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Library/refute.ML
--- 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
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Mutabelle/mutabelle_extra.ML
--- 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
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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])
 
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- 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 _ =>
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/HOL/Typerep.thy
--- 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;
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/Proof/proof_syntax.ML
--- 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))
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/Syntax/syntax_phases.ML
--- 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')]);
 
 
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/Syntax/syntax_trans.ML
--- 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);
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/logic.ML
--- 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;
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/primitive_defs.ML
--- 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;
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/pure_thy.ML
--- 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) =>
diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Pure/term.ML
--- 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;