more qualified names;
authorwenzelm
Fri Mar 21 12:34:50 2014 +0100 (2014-03-21)
changeset 562432e10a36b8d46
parent 56242 d0a9100a5a38
child 56244 3298b7a2795a
more qualified names;
src/Doc/IsarImplementation/Logic.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/Library/Countable.thy
src/HOL/Library/refute.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Typerep.thy
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/logic.ML
src/Pure/primitive_defs.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 12:14:33 2014 +0100
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 12:34:50 2014 +0100
     1.3 @@ -850,7 +850,7 @@
     1.4    @{text "#A \<equiv> A"} \\[1ex]
     1.5    @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
     1.6    @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
     1.7 -  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
     1.8 +  @{text "type :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
     1.9    @{text "(unspecified)"} \\
    1.10    \end{tabular}
    1.11    \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 21 12:14:33 2014 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 21 12:34:50 2014 +0100
     2.3 @@ -143,7 +143,7 @@
     2.4          case lhs of
     2.5            Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
     2.6              mk_eqn (f, big_lambda x rhs)
     2.7 -        | f $ Const (@{const_name TYPE}, T) =>
     2.8 +        | f $ Const (@{const_name Pure.type}, T) =>
     2.9              mk_eqn (f, Abs ("t", T, rhs))
    2.10          | Const _ => Logic.mk_equals (lhs, rhs)
    2.11          | _ => raise TERM ("lhs not of correct form", [lhs, rhs])
     3.1 --- a/src/HOL/Library/Countable.thy	Fri Mar 21 12:14:33 2014 +0100
     3.2 +++ b/src/HOL/Library/Countable.thy	Fri Mar 21 12:34:50 2014 +0100
     3.3 @@ -275,7 +275,7 @@
     3.4        let
     3.5          val ty_name =
     3.6            (case goal of
     3.7 -            (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n
     3.8 +            (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n
     3.9            | _ => raise Match)
    3.10          val typedef_info = hd (Typedef.get_info ctxt ty_name)
    3.11          val typedef_thm = #type_definition (snd typedef_info)
     4.1 --- a/src/HOL/Library/refute.ML	Fri Mar 21 12:14:33 2014 +0100
     4.2 +++ b/src/HOL/Library/refute.ML	Fri Mar 21 12:34:50 2014 +0100
     4.3 @@ -548,7 +548,7 @@
     4.4          Const (@{const_name all}, _) => t
     4.5        | Const (@{const_name "=="}, _) => t
     4.6        | Const (@{const_name "==>"}, _) => t
     4.7 -      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
     4.8 +      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
     4.9        (* HOL *)
    4.10        | Const (@{const_name Trueprop}, _) => t
    4.11        | Const (@{const_name Not}, _) => t
    4.12 @@ -713,7 +713,7 @@
    4.13        | Const (@{const_name "=="}, _) => axs
    4.14        | Const (@{const_name "==>"}, _) => axs
    4.15        (* axiomatic type classes *)
    4.16 -      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
    4.17 +      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
    4.18        (* HOL *)
    4.19        | Const (@{const_name Trueprop}, _) => axs
    4.20        | Const (@{const_name Not}, _) => axs
     5.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 12:14:33 2014 +0100
     5.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 21 12:34:50 2014 +0100
     5.3 @@ -234,7 +234,7 @@
     5.4    "nibble"]
     5.5  
     5.6  val forbidden_consts =
     5.7 - [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
     5.8 + [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
     5.9  
    5.10  fun is_forbidden_theorem (s, th) =
    5.11    let val consts = Term.add_const_names (prop_of th) [] in
     6.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 12:14:33 2014 +0100
     6.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 12:34:50 2014 +0100
     6.3 @@ -437,7 +437,7 @@
     6.4  val tvar_a = TVar tvar_a_z
     6.5  val tvar_a_name = tvar_name tvar_a_z
     6.6  val itself_name = `make_fixed_type_const @{type_name itself}
     6.7 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
     6.8 +val TYPE_name = `(make_fixed_const NONE) @{const_name Pure.type}
     6.9  val tvar_a_atype = AType ((tvar_a_name, []), [])
    6.10  val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
    6.11  
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 12:14:33 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 12:34:50 2014 +0100
     7.3 @@ -1444,7 +1444,7 @@
     7.4  fun normalized_rhs_of t =
     7.5    let
     7.6      fun aux (v as Var _) (SOME t) = SOME (lambda v t)
     7.7 -      | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
     7.8 +      | aux (c as Const (@{const_name Pure.type}, _)) (SOME t) = SOME (lambda c t)
     7.9        | aux _ _ = NONE
    7.10      val (lhs, rhs) =
    7.11        case t of
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 12:14:33 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 12:34:50 2014 +0100
     8.3 @@ -979,7 +979,7 @@
     8.4                                              (Const (mate_of_rep_fun ctxt x))
     8.5                       |> fold (add_def_axiom depth)
     8.6                               (inverse_axioms_for_rep_fun ctxt x)
     8.7 -             else if s = @{const_name TYPE} then
     8.8 +             else if s = @{const_name Pure.type} then
     8.9                 accum
    8.10               else case def_of_const thy def_tables x of
    8.11                 SOME _ =>
     9.1 --- a/src/HOL/Typerep.thy	Fri Mar 21 12:14:33 2014 +0100
     9.2 +++ b/src/HOL/Typerep.thy	Fri Mar 21 12:34:50 2014 +0100
     9.3 @@ -24,7 +24,7 @@
     9.4    let
     9.5      fun typerep_tr (*"_TYPEREP"*) [ty] =
     9.6            Syntax.const @{const_syntax typerep} $
     9.7 -            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
     9.8 +            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax Pure.type} $
     9.9                (Syntax.const @{type_syntax itself} $ ty))
    9.10        | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    9.11    in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
    9.12 @@ -34,7 +34,7 @@
    9.13    let
    9.14      fun typerep_tr' ctxt (*"typerep"*)
    9.15              (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
    9.16 -            (Const (@{const_syntax TYPE}, _) :: ts) =
    9.17 +            (Const (@{const_syntax Pure.type}, _) :: ts) =
    9.18            Term.list_comb
    9.19              (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    9.20        | typerep_tr' _ T ts = raise Match;
    10.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 12:14:33 2014 +0100
    10.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 12:34:50 2014 +0100
    10.3 @@ -133,7 +133,7 @@
    10.4              Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
    10.5        | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
    10.6            prf_of [] prf1 %% prf_of [] prf2
    10.7 -      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
    10.8 +      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
    10.9            prf_of (T::Ts) prf
   10.10        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   10.11            (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 12:14:33 2014 +0100
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 21 12:34:50 2014 +0100
    11.3 @@ -568,7 +568,7 @@
    11.4        | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
    11.5        | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
    11.6        | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
    11.7 -      | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    11.8 +      | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) =
    11.9            if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
   11.10            else mark Ts t1 $ mark Ts t2
   11.11        | mark Ts (t as t1 $ t2) =
   11.12 @@ -834,7 +834,7 @@
   11.13      ("_context_xconst", const_ast_tr false)] #>
   11.14    Sign.typed_print_translation
   11.15     [("_type_prop", type_prop_tr'),
   11.16 -    ("\\<^const>TYPE", type_tr'),
   11.17 +    ("\\<^const>Pure.type", type_tr'),
   11.18      ("_type_constraint_", type_constraint_tr')]);
   11.19  
   11.20  
    12.1 --- a/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 12:14:33 2014 +0100
    12.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Fri Mar 21 12:34:50 2014 +0100
    12.3 @@ -152,7 +152,7 @@
    12.4  
    12.5  fun mk_type ty =
    12.6    Syntax.const "_constrain" $
    12.7 -    Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);
    12.8 +    Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
    12.9  
   12.10  fun ofclass_tr [ty, cls] = cls $ mk_type ty
   12.11    | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
    13.1 --- a/src/Pure/logic.ML	Fri Mar 21 12:14:33 2014 +0100
    13.2 +++ b/src/Pure/logic.ML	Fri Mar 21 12:34:50 2014 +0100
    13.3 @@ -208,9 +208,9 @@
    13.4  
    13.5  (** types as terms **)
    13.6  
    13.7 -fun mk_type ty = Const ("TYPE", Term.itselfT ty);
    13.8 +fun mk_type ty = Const ("Pure.type", Term.itselfT ty);
    13.9  
   13.10 -fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   13.11 +fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty
   13.12    | dest_type t = raise TERM ("dest_type", [t]);
   13.13  
   13.14  fun type_map f = dest_type o f o mk_type;
    14.1 --- a/src/Pure/primitive_defs.ML	Fri Mar 21 12:14:33 2014 +0100
    14.2 +++ b/src/Pure/primitive_defs.ML	Fri Mar 21 12:34:50 2014 +0100
    14.3 @@ -37,7 +37,7 @@
    14.4  
    14.5      fun check_arg (Bound _) = true
    14.6        | check_arg (Free (x, _)) = not (is_fixed x)
    14.7 -      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
    14.8 +      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
    14.9        | check_arg _ = false;
   14.10      fun close_arg (Bound _) t = t
   14.11        | close_arg x t = Logic.all x t;
    15.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 12:14:33 2014 +0100
    15.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 12:34:50 2014 +0100
    15.3 @@ -199,12 +199,12 @@
    15.4      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    15.5      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    15.6      (Binding.name "prop", typ "prop => prop", NoSyn),
    15.7 -    (Binding.name "TYPE", typ "'a itself", NoSyn),
    15.8 +    (qualify (Binding.name "type"), typ "'a itself", NoSyn),
    15.9      (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
   15.10    #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
   15.11    #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
   15.12    #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
   15.13 -  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
   15.14 +  #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
   15.15    #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
   15.16    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   15.17    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   15.18 @@ -218,8 +218,8 @@
   15.19     [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
   15.20      (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
   15.21      (Binding.name "sort_constraint_def",
   15.22 -      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
   15.23 -      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
   15.24 +      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
   15.25 +      \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
   15.26      (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   15.27    #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
   15.28    #> fold (fn (a, prop) =>
    16.1 --- a/src/Pure/term.ML	Fri Mar 21 12:14:33 2014 +0100
    16.2 +++ b/src/Pure/term.ML	Fri Mar 21 12:34:50 2014 +0100
    16.3 @@ -816,7 +816,7 @@
    16.4  
    16.5  fun close_schematic_term t =
    16.6    let
    16.7 -    val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
    16.8 +    val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t);
    16.9      val extra_terms = map Var (add_vars t []);
   16.10    in fold lambda (extra_terms @ extra_types) t end;
   16.11