# HG changeset patch
# User wenzelm
# Date 1395503452 -3600
# Node ID 2c9f841f36b8926885001da21a29b16ee9ad0be0
# Parent  0fda98dd2c9317cb1c073934a056120b01ccb473
more antiquotations;

diff -r 0fda98dd2c93 -r 2c9f841f36b8 src/CTT/CTT.thy
--- 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
diff -r 0fda98dd2c93 -r 2c9f841f36b8 src/ZF/OrdQuant.thy
--- 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)))