# HG changeset patch
# User wenzelm
# Date 1415709849 -3600
# Node ID 762ee71498fa86933c677eb377ff8dd3e7c2c35e
# Parent  cbc2ac19d783ed50e6a48ebd37514f3edcd04ff2
more markup;

diff -r cbc2ac19d783 -r 762ee71498fa src/CCL/CCL.thy
--- 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}))
 *}
 
diff -r cbc2ac19d783 -r 762ee71498fa src/CCL/Wfd.thy
--- 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)))
 *}
diff -r cbc2ac19d783 -r 762ee71498fa src/CTT/CTT.thy
--- 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 = {*
diff -r cbc2ac19d783 -r 762ee71498fa src/LCF/LCF.thy
--- 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)))