Mercurial Mercurial > repos > isabelle / 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.
src/HOL/TLA/TLA.thy
changeset 61853 fb7756087101
parent 60754 02924903a6fd
child 69597 ff784d5a5bfb 
--- a/src/HOL/TLA/TLA.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/TLA.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -124,13 +124,13 @@
 \<close>
 
 attribute_setup temp_unlift =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close>
 attribute_setup temp_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close>
 attribute_setup temp_use =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close>
 attribute_setup try_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close>
 
 
 (* ------------------------------------------------------------------------- *)
isabelle