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/Quotient/quotient_typ.ML
changeset 45291 57cd50f98fdc
parent 45283 9e8616978d99
child 45312 6fd165677109 
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -143,7 +143,7 @@
     fun qinfo phi = Quotient_Info.transform_quotients phi quotients
 
     val lthy4 = lthy3
-      |> Local_Theory.declaration true
+      |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
isabelle