more qualified names;
authorwenzelm
Fri Mar 21 15:12:03 2014 +0100 (2014-03-21)
changeset 562443298b7a2795a
parent 56243 2e10a36b8d46
child 56245 84fc7dfa3cd4
more qualified names;
src/HOL/Tools/ATP/atp_problem_generate.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/logic.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 12:34:50 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 15:12:03 2014 +0100
     1.3 @@ -404,7 +404,7 @@
     1.4  (* These are ignored anyway by the relevance filter (unless they appear in
     1.5     higher-order places) but not by the monomorphizer. *)
     1.6  val atp_logical_consts =
     1.7 -  [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
     1.8 +  [@{const_name Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
     1.9     @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    1.10     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
    1.11  
     2.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 12:34:50 2014 +0100
     2.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 15:12:03 2014 +0100
     2.3 @@ -48,14 +48,14 @@
     2.4              SOME (equal_intr_axm % B % A %% prf2 %% prf1)
     2.5  
     2.6        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
     2.7 -        (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
     2.8 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
     2.9            _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
    2.10          ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    2.11          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    2.12  
    2.13        | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    2.14          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    2.15 -          (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    2.16 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
    2.17               _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
    2.18          ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    2.19          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
     3.1 --- a/src/Pure/logic.ML	Fri Mar 21 12:34:50 2014 +0100
     3.2 +++ b/src/Pure/logic.ML	Fri Mar 21 15:12:03 2014 +0100
     3.3 @@ -323,10 +323,10 @@
     3.4  
     3.5  (** protected propositions and embedded terms **)
     3.6  
     3.7 -val protectC = Const ("prop", propT --> propT);
     3.8 +val protectC = Const ("Pure.prop", propT --> propT);
     3.9  fun protect t = protectC $ t;
    3.10  
    3.11 -fun unprotect (Const ("prop", _) $ t) = t
    3.12 +fun unprotect (Const ("Pure.prop", _) $ t) = t
    3.13    | unprotect t = raise TERM ("unprotect", [t]);
    3.14  
    3.15  
     4.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 12:34:50 2014 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 15:12:03 2014 +0100
     4.3 @@ -191,14 +191,14 @@
     4.4      ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
     4.5      ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
     4.6    #> Sign.add_syntax ("", false)
     4.7 -   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
     4.8 +   [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
     4.9    #> Sign.add_syntax ("HTML", false)
    4.10     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    4.11    #> Sign.add_consts
    4.12     [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
    4.13      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    4.14      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    4.15 -    (Binding.name "prop", typ "prop => prop", NoSyn),
    4.16 +    (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
    4.17      (qualify (Binding.name "type"), typ "'a itself", NoSyn),
    4.18      (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
    4.19    #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
    4.20 @@ -215,7 +215,7 @@
    4.21      (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
    4.22    #> Sign.local_path
    4.23    #> (Global_Theory.add_defs false o map Thm.no_attributes)
    4.24 -   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
    4.25 +   [(Binding.name "prop_def", prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
    4.26      (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
    4.27      (Binding.name "sort_constraint_def",
    4.28        prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\