quotient_info.ML
changeset 314 3b3c5feb6b73
parent 311 77fc6f3c0343
child 318 746b17e1d6d8
--- 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