# HG changeset patch
# User kuncar
# Date 1379325297 -7200
# Node ID 71a0a8687d6cbe36cb313204c3bc7b74bf2513b7
# Parent  96814d676c49c659f7c902e77ffa7332dafd4870
make ML function for deleting quotients public

diff -r 96814d676c49 -r 71a0a8687d6c src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 11:54:57 2013 +0200
@@ -15,6 +15,7 @@
   val transform_quotient: morphism -> quotient -> quotient
   val lookup_quotients: Proof.context -> string -> quotient option
   val update_quotients: string -> quotient -> Context.generic -> Context.generic
+  val delete_quotients: thm -> Context.generic -> Context.generic
   val print_quotients: Proof.context -> unit
 
   val get_invariant_commute_rules: Proof.context -> thm list