# HG changeset patch
# User wenzelm
# Date 1395411123 -3600
# Node ID 3298b7a2795a63dc415e94c8c2c3e6e3246e6ba3
# Parent  2e10a36b8d46e81fb70731c28b59f546089abf33
more qualified names;

diff -r 2e10a36b8d46 -r 3298b7a2795a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 15:12:03 2014 +0100
@@ -404,7 +404,7 @@
 (* 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 Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
    @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
 
diff -r 2e10a36b8d46 -r 3298b7a2795a src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 21 15:12:03 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 %%
diff -r 2e10a36b8d46 -r 3298b7a2795a src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/Pure/logic.ML	Fri Mar 21 15:12:03 2014 +0100
@@ -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]);
 
 
diff -r 2e10a36b8d46 -r 3298b7a2795a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 21 15:12:03 2014 +0100
@@ -191,14 +191,14 @@
     ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
     ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
   #> Sign.add_syntax ("", false)
-   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
+   [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   #> Sign.add_syntax ("HTML", false)
    [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts
    [(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),
+    (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 "==" ("==", typ "'a => 'a => prop") []
@@ -215,7 +215,7 @@
     (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 Pure.type :: 'a itself) ==\