--- a/NEWS Wed Aug 18 12:26:15 2010 +0200
+++ b/NEWS Wed Aug 18 12:27:39 2010 +0200
@@ -131,6 +131,16 @@
similar to inductive_cases.
+*** FOL ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
+*** ZF ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
*** ML ***
* ML antiquotations @{theory} and @{theory_ref} refer to named
--- a/src/FOL/IFOL.thy Wed Aug 18 12:26:15 2010 +0200
+++ b/src/FOL/IFOL.thy Wed Aug 18 12:27:39 2010 +0200
@@ -28,8 +28,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -87,8 +85,6 @@
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
-local
-
finalconsts
False All Ex
"op ="
--- a/src/FOLP/IFOLP.thy Wed Aug 18 12:26:15 2010 +0200
+++ b/src/FOLP/IFOLP.thy Wed Aug 18 12:27:39 2010 +0200
@@ -12,8 +12,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -63,8 +61,6 @@
nrm :: p
NRM :: p
-local
-
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
ML {*
--- a/src/ZF/Datatype_ZF.thy Wed Aug 18 12:26:15 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy Wed Aug 18 12:27:39 2010 +0200
@@ -61,7 +61,7 @@
struct
val trace = Unsynchronized.ref false;
- fun mk_new ([],[]) = Const("True",FOLogic.oT)
+ fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
| mk_new (largs,rargs) =
Balanced_Tree.make FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -85,7 +85,7 @@
if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
- else Const("False",FOLogic.oT)
+ else Const(@{const_name False},FOLogic.oT)
else raise Match
val _ =
if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
--- a/src/ZF/Tools/induct_tacs.ML Wed Aug 18 12:26:15 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Aug 18 12:27:39 2010 +0200
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/inductive_package.ML Wed Aug 18 12:26:15 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Aug 18 12:27:39 2010 +0200
@@ -102,7 +102,7 @@
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
- fun dest_tprop (Const("Trueprop",_) $ P) = P
+ fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
Syntax.string_of_term ctxt Q);
--- a/src/ZF/Tools/typechk.ML Wed Aug 18 12:26:15 2010 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Aug 18 12:27:39 2010 +0200
@@ -75,7 +75,7 @@
if length rls <= maxr then resolve_tac rls i else no_tac
end);
-fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
+fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;