diff -r df225aa45770 -r 34ad627ac5d5 QuotMain.thy --- a/QuotMain.thy Wed Nov 04 10:31:20 2009 +0100 +++ b/QuotMain.thy Wed Nov 04 10:43:33 2009 +0100 @@ -1014,6 +1014,7 @@ end *} + ML {* fun lift_thm lthy qty qty_name rsp_thms defs t = let val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;