--- 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}]
--- 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 %%
--- 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]);
--- 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) ==\