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/Pure/Isar/method.ML
changeset 64556 851ae0e7b09c
parent 63527 59eff6e56d81
child 67147 dea94b1aabc3 
--- a/src/Pure/Isar/method.ML	Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/method.ML	Tue Dec 13 11:51:42 2016 +0100
@@ -393,7 +393,7 @@
 
 val _ =
   Theory.setup
-    (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", @{here}), get_facts_generic));
+    (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", \<^here>), get_facts_generic));
 
 
 (* method text *)
@@ -497,7 +497,7 @@
     val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
   in map Token.closure src' end;
 
-val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
+val closure = Config.bool (Config.declare ("Method.closure", \<^here>) (K (Config.Bool true)));
 
 fun method_cmd ctxt =
   check_src ctxt #>
@@ -608,7 +608,7 @@
 (* sections *)
 
 val old_section_parser =
-  Config.bool (Config.declare ("Method.old_section_parser", @{here}) (K (Config.Bool false)));
+  Config.bool (Config.declare ("Method.old_section_parser", \<^here>) (K (Config.Bool false)));
 
 local
isabelle