diff -r 4cf79f70efec -r 3b3c5feb6b73 quotient_info.ML --- 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