# HG changeset patch
# User wenzelm
# Date 1213191620 -7200
# Node ID 443c199531379454cca827eedbbf95dc2f9ea2fb
# Parent  0337828b7815d6973e15b2b83b07567949ee619a
more antiquotations;

diff -r 0337828b7815 -r 443c19953137 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/CCL.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -414,8 +414,7 @@
   done
 
 ML {*
-  local val po_coinduct = thm "po_coinduct"
-  in fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i end
+  fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
 *}
 
 
@@ -460,13 +459,8 @@
   done
 
 ML {*
-  local
-    val eq_coinduct = thm "eq_coinduct"
-    val eq_coinduct3 = thm "eq_coinduct3"
-  in
-    fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i
-    fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i
-  end
+  fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
+  fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
 *}
 
 
diff -r 0337828b7815 -r 443c19953137 src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/Hered.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -97,8 +97,7 @@
   done
 
 ML {*
-  local val HTT_coinduct = thm "HTT_coinduct"
-  in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end
+  fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
 *}
 
 lemma HTT_coinduct3:
@@ -108,17 +107,12 @@
   done
 
 ML {*
-local
-  val HTT_coinduct3 = thm "HTT_coinduct3"
-  val HTTgen_def = thm "HTTgen_def"
-in
+val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
 
-val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3
-
-fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i
+fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
 
 val HTTgenIs =
-  map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono"))
+  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   ["true : HTTgen(R)",
    "false : HTTgen(R)",
    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
@@ -130,8 +124,6 @@
    "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]
-
-end
 *}
 
 ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
diff -r 0337828b7815 -r 443c19953137 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/Wfd.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -54,10 +54,8 @@
   done
 
 ML {*
-  local val wfd_strengthen_lemma = thm "wfd_strengthen_lemma" in
   fun wfd_strengthen_tac s i =
-    res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN assume_tac (i+1)
-  end
+    res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
 *}
 
 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
diff -r 0337828b7815 -r 443c19953137 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/Sequents/LK0.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -155,21 +155,13 @@
   by (rule exchLS)
 
 ML {*
-local
-  val thinR = thm "thinR"
-  val thinL = thm "thinL"
-  val cut = thm "cut"
-in
-
 (*Cut and thin, replacing the right-side formula*)
 fun cutR_tac s i =
-  res_inst_tac [ ("P", s) ] cut i  THEN  rtac thinR i
+  res_inst_tac [ ("P", s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
 
 (*Cut and thin, replacing the left-side formula*)
 fun cutL_tac s i =
-  res_inst_tac [("P", s)] cut i  THEN  rtac thinL (i+1)
-
-end
+  res_inst_tac [("P", s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
 *}