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_def.ML
changeset 57534 d2617d923aa1
parent 57399 cfc19f0a6261
child 57567 d554b0097ad4 
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Jul 09 11:35:52 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Jul 09 11:35:52 2014 +0200
@@ -722,7 +722,8 @@
       end;
 
     fun maybe_restore lthy_old lthy =
-      lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
+      lthy |> not (Theory.eq_thy (pairself Proof_Context.theory_of (lthy_old, lthy)))
+        ? Local_Theory.restore;
 
     val map_bind_def =
       (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
isabelle