--- a/src/CTT/CTT.thy Sat Mar 22 15:58:27 2014 +0100
+++ b/src/CTT/CTT.thy Sat Mar 22 16:50:52 2014 +0100
@@ -328,9 +328,9 @@
local
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
+fun is_rigid_elem (Const(@{const_name Elem},_) $ a $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(@{const_name Eqelem},_) $ a $ _ $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(@{const_name Type},_) $ a) = not(is_Var (head_of a))
| is_rigid_elem _ = false
in
--- a/src/ZF/OrdQuant.thy Sat Mar 22 15:58:27 2014 +0100
+++ b/src/ZF/OrdQuant.thy Sat Mar 22 16:50:52 2014 +0100
@@ -357,9 +357,8 @@
ML
{*
val Ord_atomize =
- atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
- ZF_conn_pairs,
- ZF_mem_pairs);
+ atomize ([(@{const_name oall}, @{thms ospec}), (@{const_name rall}, @{thms rspec})] @
+ ZF_conn_pairs, ZF_mem_pairs);
*}
declaration {* fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))