--- a/src/CCL/CCL.thy Tue Nov 11 13:40:13 2014 +0100
+++ b/src/CCL/CCL.thy Tue Nov 11 13:44:09 2014 +0100
@@ -473,7 +473,7 @@
done
method_setup eq_coinduct3 = {*
- Scan.lift Args.name >> (fn s => fn ctxt =>
+ Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3}))
*}
--- a/src/CCL/Wfd.thy Tue Nov 11 13:40:13 2014 +0100
+++ b/src/CCL/Wfd.thy Tue Nov 11 13:44:09 2014 +0100
@@ -47,7 +47,7 @@
done
method_setup wfd_strengthen = {*
- Scan.lift Args.name >> (fn s => fn ctxt =>
+ Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)))
*}
--- a/src/CTT/CTT.thy Tue Nov 11 13:40:13 2014 +0100
+++ b/src/CTT/CTT.thy Tue Nov 11 13:44:09 2014 +0100
@@ -480,7 +480,7 @@
*}
method_setup NE = {*
- Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+ Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
*}
method_setup pc = {*
--- a/src/LCF/LCF.thy Tue Nov 11 13:40:13 2014 +0100
+++ b/src/LCF/LCF.thy Tue Nov 11 13:44:09 2014 +0100
@@ -319,7 +319,7 @@
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
method_setup induct = {*
- Scan.lift Args.name >> (fn v => fn ctxt =>
+ Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
REPEAT (resolve_tac @{thms adm_lemmas} i)))