--- a/quotient_info.ML Thu Nov 12 12:07:33 2009 +0100
+++ b/quotient_info.ML Thu Nov 12 13:56:07 2009 +0100
@@ -81,7 +81,7 @@
val quotdata_lookup_thy = Symtab.lookup o QuotData.get
val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
-fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
+fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
fun quotdata_update qty_name (qty, rty, rel, equiv_thm) =
@@ -164,4 +164,4 @@
end; (* structure *)
-open Quotient_Info
\ No newline at end of file
+open Quotient_Info