src/CCL/Type.thy
changeset 32010 cb1a1c94b4cd
parent 30607 c3d1590debd8
child 32149 ef59550a55d3
--- a/src/CCL/Type.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/Type.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -428,7 +428,7 @@
 
 ML {*
 
-val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono"))
+val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
   ["<true,true> : POgen(R)",
    "<false,false> : POgen(R)",
    "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
@@ -443,9 +443,9 @@
 
 fun POgen_tac ctxt (rla,rlb) i =
   SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
-  rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
-  (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
-    (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
+  rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
+  (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
+    (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
 
 *}
 
@@ -458,7 +458,7 @@
 
 ML {*
 
-val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono"))
+val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
   ["<true,true> : EQgen(R)",
    "<false,false> : EQgen(R)",
    "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",