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/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
changeset 69593 3dda49e08b9d
parent 67710 cc2db3239932 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -132,7 +132,7 @@
 
     val simp_ctxt = (ctxt
         |> Context_Position.set_visible false
-        |> put_simpset (simpset_of (Proof_Context.init_global @{theory Main}))
+        |> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\<open>Main\<close>))
         |> Raw_Simplifier.add_cong @{thm if_cong})
       addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def ::
         @{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @
isabelle