Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_permeq.ML
changeset 3229 b52e8651591f
parent 3183 313e6f2cdd89
child 3239 67370521c09c 
--- a/Nominal/nominal_permeq.ML	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_permeq.ML	Thu Mar 13 09:21:31 2014 +0000
@@ -22,8 +22,8 @@
   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
 
-  val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
-  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
+  val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method
+  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method
   val args_parser: (thm list * string list) context_parser
 
   val trace_eqvt: bool Config.T
@@ -219,9 +219,9 @@
    Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];
 
 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
-  (Scan.repeat (Args.const true))) []
+  (Scan.repeat (Args.const {proper = true, strict = true}))) []
 
-val args_parser =  add_thms_parser -- exclude_consts_parser 
+val args_parser = add_thms_parser -- exclude_consts_parser 
 
 fun perm_simp_meth (thms, consts) ctxt =
   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts)))
nominal2